proposition: Lemma of_nat_via_N x : of_nat x = of_N (N.of_nat x).
proof: Proof. destruct (of_nat x) as [b|] eqn:H1. { rewrite to_of_nat_iff in H1; subst. destruct b; reflexivity. } { rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff in H1. symmetry; rewrite of_N_None_iff, <- N.compare_lt_iff. rewrite N2Nat.inj_compare, Nat2N.id; assumption. } Qed.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte