proposition: Lemma eqFaM_Equiv : equivalence eqFaM.
proof: Proof. red in |- *. split; [ try assumption | idtac ]. exact eqFaM_refl. red in |- *. split; [ try assumption | idtac ]. exact eqFaM_trans. exact eqFaM_sym. Qed.
imports: Monoid_cat Sgroup_facts Monoid_facts Monoid_util Abelian_group_facts