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