right and left cancellation in groups

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index 9d98aea4d9d232758c1145db350da6a78f71d3a6..0f759434f85fd07b48935e418cd99a35664878e7 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/algebra/groups/".
 
 include "algebra/monoids.ma".
+include "nat/le_arith.ma".
 
 record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
  { opp_is_left_inverse: is_left_inverse M opp;
@@ -35,19 +36,20 @@ for @{ 'gopp $x }.
 interpretation "Group inverse" 'gopp x =
  (cic:/matita/algebra/groups/opp.con _ x).
 
-definition left_cancellable :=
- \lambda T:Type. \lambda op: T -> T -> T.
-  \forall x,y,z. op x y = op x z -> y = z.
+definition left_cancellable ≝
+ λT:Type. λop: T -> T -> T.
+  ∀x. injective ? ? (op x).
   
-definition right_cancellable :=
- \lambda T:Type. \lambda op: T -> T -> T.
-  \forall x,y,z. op y x = op z x -> y = z.
+definition right_cancellable ≝
+ λT:Type. λop: T -> T -> T.
+  ∀x. injective ? ? (λz.op z x).
   
 theorem eq_op_x_y_op_x_z_to_eq:
- \forall G:Group. left_cancellable G (op G).
+ ∀G:Group. left_cancellable G (op G).
 intros;
 unfold left_cancellable;
-intros;
+unfold injective;
+intros (x y z);
 rewrite < (e_is_left_unit ? ? (monoid_properties G));
 rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
 rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
@@ -57,16 +59,42 @@ apply eq_f;
 assumption.
 qed.
 
-(*
+
 theorem eq_op_x_y_op_z_y_to_eq:
- \forall G:Group. right_cancellable G (op G).
+ ∀G:Group. right_cancellable G (op G).
+intros;
+unfold right_cancellable;
+unfold injective;
+simplify;fold simplify (op G); 
+intros (x y z);
+rewrite < (e_is_right_unit ? ? (monoid_properties G));
+rewrite < (e_is_right_unit ? ? (monoid_properties G) z);
+rewrite < (opp_is_right_inverse ? ? (group_properties G) x);
+rewrite < (semigroup_properties G);
+rewrite < (semigroup_properties G);
+rewrite > H;
+reflexivity.
 qed.
 
-definition has_cardinality :=
- \lambda T:Type. \lambda n:nat.
-  \exists f. injective T nat f.
+(*
+record enumerable (T:Type) : Type ≝
+ { order: nat;
+   repr: nat → T;
+   repr_inj: ∀n,n'. n≤order → n'≤order → repr n ≠ repr n';
+   repr_sur: ∀x.∃n.n≤order ∧ repr n = x
+ }.
+ 
 
-definition finite :=
- \lambda T:Type.
-  \exists f: T -> {n|n<
-*)
+theorem foo:
+ ∀G:SemiGroup.
+  enumerable (carrier G) →
+   left_cancellable (carrier G) (op G) →
+    right_cancellable (carrier G) (op G) →
+     ∃e:G. is_left_unit ? e.
+intros (G H);
+unfold left_cancellable in H1;
+letin x ≝ (repr ? H O);
+letin f ≝ (λy.x·(repr ? H y));
+generalize in match (H1 x);
+intro;
+*)
\ No newline at end of file