proposition: Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.
proof: Proof. constructor. exact (Radd_0_l BigZring). exact (Radd_comm BigZring). exact (Radd_assoc BigZring). exact (Rmul_1_l BigZring). exact BigZ.mul_0_l. exact (Rmul_comm BigZring). exact (Rmul_assoc BigZring). exact BigZ.mul_add_distr_r. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ)