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