proposition: Lemma GROUP_unit_inverse : Equal (group_inverse _ (monoid_unit G)) (monoid_unit G).
proof: Proof. apply Trans with (sgroup_law _ (group_inverse _ (monoid_unit G)) (monoid_unit G)); auto with algebra. Qed.
imports: Group_cat Sgroup_facts Monoid_facts