proposition: Lemma group_quo_eqrel_equiv : equivalence group_quo_eqrel.
proof: Proof. red in Hnormal. red in |- *. split; [ try assumption | idtac ]. red in |- *. intros x; red in |- *. simpl in |- *. unfold app_rel, group_quo_eq in |- *. apply in_part_comp_l with (sgroup_law G x (sgroup_law G (monoid_unit G) (group_inverse G x))); auto with algebra. red in |- *. split; [ try assumption | idtac ]. red in |- *. simpl in |- *. unfold app_rel, group_quo_eq in |- *. intros x y z H' H'0; try assumption. apply in_part_comp_l with (sgroup_law G (sgroup_law G x (group_inverse G y)) (sgroup_law G y (group_inverse G z))); auto with algebra. apply Trans with (sgroup_law G x (sgroup_law G (group_inverse G y) (sgroup_law G y (group_inverse G z)))); auto with algebra. apply Trans with (sgroup_law G x (sgroup_law G (sgroup_law G (group_inverse G y) y) (group_inverse G z))); auto with algebra. apply Trans with (sgroup_law G x (sgroup_law G (monoid_unit G) (group_inverse G z))); auto with algebra. red in |- *. simpl in |- *. unfold app_rel, group_quo_eq in |- *. intros x y H'; try assumption. apply in_part_comp_l with (group_inverse G (sgroup_law G x (group_inverse G y))); auto with algebra. apply Trans with (sgroup_law G (group_inverse G (group_inverse G y)) (group_inverse G x)); auto with algebra. Qed.
imports: Sub_group Group_util