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