λG.λC,C':left_coset G.
∀x.((element ? C)·x \sub (subgrp ? C)) ∈ C'.
-interpretation "Left cosets equality" 'eq C C' =
- (cic:/matita/algebra/groups/left_coset_eq.con _ C C').
+interpretation "Left cosets equality" 'eq t C C' =
+ (cic:/matita/algebra/groups/left_coset_eq.con t C C').
definition left_coset_disjoint ≝
λG.λC,C':left_coset G.
∀G.∀x:Type_OF_Group G.∀H:subgroup G.x ∈ (x*H).
intros;
simplify;
-apply (ex_intro ? ? 1);
+apply (ex_intro ? ? ⅇ);
rewrite > morphism_to_eq_f_1_1;
rewrite > (e_is_right_unit ? G);
reflexivity.