theorem Fin.ofNat_eq (n : Nat) (h : n < UInt32.size) : Fin.ofNat UInt32.size n = ⟨n, h⟩

theorem Fin.ofNat_val_eq (n : Nat) (h : n < UInt32.size) : ↑(Fin.ofNat UInt32.size n) = n

theorem Fin.toNat_ofNat_eq (n : Fin UInt32.size) : Fin.ofNat UInt32.size ↑n = n

theorem Fin.ofNat_val_add (n m : Fin UInt32.size) (h : ↑n + ↑m < UInt32.size) : Fin.ofNat UInt32.size (↑n + ↑m) = n + m