set "baseuri" "cic:/matita/algebra/groups/".
+include "algebra/monoids.ma".
+
+record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
+ { opp_is_left_inverse: is_left_inverse M opp;
+ opp_is_right_inverse: is_right_inverse M opp
+ }.
+
+record Group : Type ≝
+ { monoid: Monoid;
+ opp: monoid -> monoid;
+ group_properties: isGroup ? opp
+ }.
+
+coercion cic:/matita/algebra/groups/monoid.con.
+
+notation "hvbox(x \sup (-1))" with precedence 89
+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 right_cancellable :=
+ \lambda T:Type. \lambda op: T -> T -> T.
+ \forall x,y,z. op y x = op z x -> y = z.
+
+theorem eq_op_x_y_op_x_z_to_eq:
+ \forall G:Group. left_cancellable G (op G).
+intros;
+unfold left_cancellable;
+intros;
+rewrite < (e_is_left_unit ? ? (monoid_properties G));
+fold simplify (e G);
+rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
+fold simplify (e G);
+rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
+fold simplify (opp G);
+rewrite > (semigroup_properties G);
+fold simplify (op G);
+rewrite > (semigroup_properties G);
+fold simplify (op G);
+apply eq_f;
+assumption.
+qed.
+
+(*
+theorem eq_op_x_y_op_z_y_to_eq:
+ \forall G:Group. right_cancellable G (op G).
+qed.
+
+definition has_cardinality :=
+ \lambda T:Type. \lambda n:nat.
+ \exists f. injective T nat f.
+
+definition finite :=
+ \lambda T:Type.
+ \exists f: T -> {n|n<
+*)