proposition: Lemma is_CMonoid_proof_irr : forall (S:CSetoid) (Zero:S) (plus : CSetoid_bin_op S) (p q : associative plus), is_CMonoid (Build_CSemiGroup S plus p) Zero -> is_CMonoid (Build_CSemiGroup S plus q) Zero.
proof: Proof. intros S one mult p q H. elim H; intros runit0 lunit0. simpl in runit0. simpl in lunit0. apply Build_is_CMonoid; simpl in |- *; assumption. Qed.
imports: Coq.Arith.Euclid CoRN.model.Zmod.Cmod CoRN.algebra.CSemiGroups CoRN.tactics.csetoid_rewrite CoRN.model.structures.Nsec CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms