-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
+letin f ≝ (λn.index_of ? H ((repr ? H O)·(repr ? H n)));
+cut (∀n.n ≤ order ? H → ∃m.f m = n);
+[ letin EX ≝ (Hcut O ?);
+ [ apply le_O_n
+ | clearbody EX;
+ clear Hcut;
+ unfold f in EX;
+ elim EX;
+ letin HH ≝ (eq_f ? ? (repr ? H) ? ? H3);
+ clearbody HH;
+ rewrite > (repr_index_of ? H) in HH;
+ apply (ex_intro ? ? (repr ? H a));
+ letin GOGO ≝ (refl_eq ? (repr ? H O));
+ clearbody GOGO;
+ rewrite < HH in GOGO;
+ rewrite < HH in GOGO:(? ? % ?);
+ rewrite > (semigroup_properties G) in GOGO;
+ letin GaGa ≝ (H1 ? ? ? GOGO);
+ clearbody GaGa;
+ clear GOGO;
+ constructor 1;
+ [ unfold is_left_unit; intro;
+ letin GaxGax ≝ (refl_eq ? ((repr ? H a)·x));
+ clearbody GaxGax;
+ rewrite < GaGa in GaxGax:(? ? % ?);
+ rewrite > (semigroup_properties G) in GaxGax;
+ apply (H1 ? ? ? GaxGax)
+ | unfold is_right_unit; intro;
+ letin GaxGax ≝ (refl_eq ? (x·(repr ? H a)));
+ clearbody GaxGax;
+ rewrite < GaGa in GaxGax:(? ? % ?);
+ rewrite < (semigroup_properties G) in GaxGax;
+ apply (H2 ? ? ? GaxGax)
+ ]
+|
+].
\ No newline at end of file