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