proposition: Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.
proof: Proof. constructor. exact Zplus_0_l. exact Zplus_comm. exact Zplus_assoc. exact Zmult_1_l. exact Zmult_0_l. exact Zmult_comm. exact Zmult_assoc. exact Zmult_plus_distr_l. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith)