proposition: Lemma eqFG_Equiv : equivalence eqFG.
proof: Proof. red in |- *. split; [ try assumption | idtac ]. exact eqFG_refl. red in |- *. split; [ try assumption | idtac ]. exact eqFG_trans. exact eqFG_sym. Qed.
imports: Group_util