proposition: Lemma Inverses_equiv : Equivalence Inverses_eq.
proof: Proof. apply Build_Equivalence. unfold Reflexive in |- *. intro x; unfold Inverses_eq in |- *. apply Refl. apply Build_Partial_equivalence. unfold Transitive in |- *. intros x y z H1 H2; unfold Inverses_eq in |- *. apply Trans with (Inv_elt_l y); assumption. unfold Symmetric in |- *. intros x y H; unfold Inverses_eq in |- *. apply Sym; assumption. Qed.
imports: Group