proposition: Theorem nat_of_N_eq : forall n m, nat_of_N n = nat_of_N m -> n = m.
proof: Proof. intros ? ? H; apply (f_equal N_of_nat) in H; autorewrite with N in *; assumption. Qed.
imports: Coq.Bool.Bool Coq.Classes.Morphisms Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith Coq.ZArith.ZArith