proposition: Lemma GROUP_inverse_inverse : forall x : G, Equal (group_inverse _ (group_inverse _ x)) x.
proof: Proof. intros x; try assumption. apply GROUP_reg_right with (group_inverse _ x). apply Trans with (monoid_unit G); auto with algebra. Qed.
imports: Group_cat Sgroup_facts Monoid_facts