proposition: Lemma eqFaG_Equiv : equivalence eqFaG.
proof: Proof. red in |- *. split; [ try assumption | idtac ]. exact eqFaG_refl. red in |- *. split; [ try assumption | idtac ]. exact eqFaG_trans. exact eqFaG_sym. Qed.
imports: Group_util Abelian_group_facts