proposition: Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.
proof: Proof. constructor; intros. compute; trivial. apply A_plus_comm. apply A_plus_assoc. destruct n; compute; trivial. compute; trivial. apply A_mult_comm. apply A_mult_assoc. apply A_mult_plus_distr. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ)