-(*theorem foo:
- \forall G:Group. \forall x1,x2:G. \forall H:subgroup G.
- x1*x2^-1 \nin H \to x1*H does_not_overlap x2*H
-
-theorem foo:
- \forall x:G. \forall H:subgroup G. x \in x*H
-
-definition disjoinct
- (T: Type) (n:nat) (S: \forall x:nat. x < n -> {S:Type * (S -> T)})
-:=
- \forall i,j:nat. i < n \to j < n \to ...
+theorem Not_member_of_subgroup_to_left_coset_disjoint:
+ ∀G.∀x,y.∀H:subgroup G.(x \sup -1 ·y) ∉ H → x*H ∥ y*H.
+intros;
+simplify;
+unfold Not;
+intros (x');
+apply H1;
+unfold member_of_subgroup;
+elim H2;
+apply (ex_intro ? ? (x'·a \sup -1));
+rewrite > f_morph;
+apply (eq_op_x_y_op_z_y_to_eq ? (a \sub H));
+rewrite > (op_associative ? G);
+rewrite < H3;
+rewrite > (op_associative ? G);
+rewrite < f_morph;
+rewrite > (inv_is_left_inverse ? H);
+rewrite < (op_associative ? G);
+rewrite > (inv_is_left_inverse ? G);
+rewrite > (e_is_left_unit ? G);
+rewrite < (f_morph ? ? H);
+rewrite > (e_is_right_unit ? H);
+reflexivity.
+qed.