proposition: Lemma nat_morph_N : semi_morph 0 1 plus mult (eq (A:=nat)) 0%N 1%N N.add N.mul N.eqb N.to_nat.
proof: Proof. constructor;trivial. - exact N2Nat.inj_add. - exact N2Nat.inj_mul. - intros x y H. apply N.eqb_eq in H. now subst. Qed.
imports: PeanoNat BinNat Nnat Ring