proposition: Lemma Nsth : Setoid_Theory N (@eq N).
proof: Proof. Proof (Eqsth N). Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N). Proof (Eq_s_ext N.add N.mul). Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N). Proof. constructor. - exact N.add_0_l. - exact N.add_comm. - exact N.add_assoc. - exact N.mul_1_l. - exact N.mul_0_l. - exact N.mul_comm. - exact N.mul_assoc. - exact N.mul_add_distr_r. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom