proposition: Lemma GROUP_inverse_r : forall x : G, Equal (sgroup_law _ x (group_inverse _ x)) (monoid_unit G).
proof: Proof. intros; apply (group_inverse_r_prf G x); auto with algebra. Qed.
imports: Group_cat Sgroup_facts Monoid_facts