proposition: Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.
proof: Proof. constructor; intros. apply orb_false_l. apply orb_comm. apply orb_assoc. apply andb_true_l. apply andb_false_l. apply andb_comm. apply andb_assoc. apply andb_orb_distrib_l. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ) CoLoR(ZUtil)