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