proposition: Lemma GROUP_law_inverse : forall x y : G, Equal (sgroup_law _ x y) (monoid_unit G) -> Equal (group_inverse _ x) y.
proof: Proof. intros x y H'; try assumption. apply GROUP_reg_left with x. apply Trans with (monoid_unit G); auto with algebra. Qed.
imports: Group_cat Sgroup_facts Monoid_facts