proposition: Lemma normal_com_in : forall x y : G, in_part (sgroup_law _ x y) H -> in_part (sgroup_law _ y x) H.
proof: Proof. intros x y H'; try assumption. apply in_part_comp_l with (sgroup_law G y (sgroup_law G (sgroup_law G x y) (group_inverse G y))); auto with algebra. apply SGROUP_comp; auto with algebra. apply Trans with (sgroup_law G x (sgroup_law G y (group_inverse G y))); auto with algebra. apply Trans with (sgroup_law G x (monoid_unit G)); auto with algebra. Qed.
imports: Sub_group Group_util