repr_index_of: ∀x. repr (index_of x) = x
}.
-notation < "hvbox(C \sub i)" with precedence 89
+notation "hvbox(C \sub i)" with precedence 89
for @{ 'repr $C $i }.
+(* CSC: multiple interpretations in the same file are not considered in the
+ right order
interpretation "Finite_enumerable representation" 'repr C i =
- (cic:/matita/algebra/groups/repr.con C _ i).
+ (cic:/matita/algebra/groups/repr.con C _ i).*)
-notation < "hvbox(|C|)" with precedence 89
+notation "hvbox(|C|)" with precedence 89
for @{ 'card $C }.
interpretation "Finite_enumerable order" 'card C =
right_cancellable ? (op G) →
∃e:G. isMonoid G e.
intros;
-letin f ≝
- (λn.index_of G (is_finite_enumerable G)
- (op G
- (repr (Type_of_finite_enumerable_SemiGroup G) (is_finite_enumerable G) O)
- (repr (Type_of_finite_enumerable_SemiGroup G) (is_finite_enumerable G) n)));
+letin f ≝ (λn.ι(G \sub O · G \sub n));
cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
[ letin EX ≝ (Hcut O ?);
[ apply le_O_n
letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
clearbody HH;
rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
- apply (ex_intro ? ? (repr ? (is_finite_enumerable G) a));
+ apply (ex_intro ? ? (G \sub a));
letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
clearbody GOGO;
rewrite < HH in GOGO;
clear GOGO;
constructor 1;
[ unfold is_left_unit; intro;
- letin GaxGax ≝ (refl_eq ? ((repr ? (is_finite_enumerable G) a)·x));
+ letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
rewrite > (semigroup_properties G) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
- letin GaxGax ≝ (refl_eq ? (x·(repr ? (is_finite_enumerable G) a)));
+ letin GaxGax ≝ (refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
rewrite < (semigroup_properties G) in GaxGax;