proposition: Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
proof: Proof. constructor. - exact Nat.add_0_l. - exact Nat.add_comm. - exact Nat.add_assoc. - exact Nat.mul_1_l. - exact Nat.mul_0_l. - exact Nat.mul_comm. - exact Nat.mul_assoc. - exact Nat.mul_add_distr_r. Qed.
imports: PeanoNat BinNat Nnat Ring