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

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

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

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

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