Definition C_as_CSetoid (k n :Z)(H:(n>0)%Z)(H0:(k>= 0)%Z):CSetoid
:= ZCSetoid_of_less (k+n).
Definition C_plus (k n:Z) (H:(n>0)%Z)(H0:(k>=0)%Z):
C_as_CSetoid k n H H0-> C_as_CSetoid k n H H0-> C_as_CSetoid k n H H0.
Defined.
Lemma C_plus_strext:
forall (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z),(bin_fun_strext (C_as_CSetoid k n H H0)
(C_as_CSetoid k n H H0) (C_as_CSetoid k n H H0) (C_plus k n H H0)).
Definition C_plus_as_bin_fun (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z):=
(Build_CSetoid_bin_fun (C_as_CSetoid k n H H0) (C_as_CSetoid k n H H0)
(C_as_CSetoid k n H H0) (C_plus k n H H0) (C_plus_strext k n H H0)).
Lemma C_plus_is_CSemiGroup:forall (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z),
(is_CSemiGroup (C_as_CSetoid k n H H0)(C_plus_as_bin_fun k n H H0)).
Definition C_as_CSemiGroup (k n :Z)(H:(n>0)%Z)(H0:(k>=0)%Z):=
(Build_CSemiGroup (C_as_CSetoid k n H H0)(C_plus_as_bin_fun k n H H0)
(C_plus_is_CSemiGroup k n H H0)).
Definition C0 (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z):(C_as_CSetoid k n H H0).
Defined.
Lemma O_is_rht_unit_C: forall (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z),
(is_rht_unit (C_plus_as_bin_fun k n H H0) (C0 k n H H0)).
Lemma O_is_lft_unit_C: forall (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z),
(is_lft_unit (C_plus_as_bin_fun k n H H0) (C0 k n H H0)).
Definition C_is_CMonoid (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z):=
(Build_is_CMonoid (C_as_CSemiGroup k n H H0)(C0 k n H H0)
(O_is_rht_unit_C k n H H0)(O_is_lft_unit_C k n H H0)).
Definition C_as_CMonoid ( k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z):=
(Build_CMonoid (C_as_CSemiGroup k n H H0)(C0 k n H H0)(C_is_CMonoid k n H H0)).
Definition c (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z)(H1:(1<k+n)%Z):
(C_as_CSetoid k n H H0).
Defined.
Definition cm (k n:Z)(m:nat)(H:(n>0)%Z)(H0:(k>=0)%Z)(H1:((Z_of_nat m)<k+n)%Z):
(C_as_CSetoid k n H H0).
Defined.
Lemma c_plus: forall(k n:Z)(m:nat)(H:(n>0)%Z)(H0:((Z_of_nat (S m))<k+n)%Z)
(H1:((Z_of_nat m)<k+n)%Z)(H2:(k>=0)%Z)(H3:(1<k+n)%Z), ((C_plus_as_bin_fun k n H H2)(cm k n m H H2 H1)(c k n H H2 H3))[=]
(cm k n (S m) H H2 H0).
Lemma power_C_plus:
forall (k n:Z) (m:nat)(H:(n>0)%Z)(H0:(1<k+n)%Z)(H1:(k>=0)%Z),
@power_CMonoid (C_as_CMonoid k n H H1)(c k n H H1 H0)(S m)[=]
(@power_CMonoid (C_as_CMonoid k n H H1)(c k n H H1 H0) m)[+](c k n H H1 H0).
Lemma power_c:forall (m:nat)(k n:Z)(H:(n>0)%Z)(H0:(1<k+n)%Z)
(H1:(m<k+n)%Z)(H2:(k>=0)%Z),
@power_CMonoid (C_as_CMonoid k n H H2)(c k n H H2 H0) m [=]
(cm k n m H H2 H1).
Lemma cyclic_C:(forall (k n:Z)(H:(n>0)%Z)(H0:(k>=0)%Z),
cyclic (C_as_CMonoid k n H H0)):CProp.
Definition to_C:
forall (M:CMonoid)(u:M)(k l:nat)(H2:((Z_of_nat (l-k))>0)%Z)
(H3:((Z_of_nat k)>=0)%Z),(is_generator M u)->
(k<l and
(power_CMonoid u k [=] power_CMonoid u l)
and ((forall (k0 l0:nat), (k0<>l0 and (k0<k or (k0=k and l0<l)))->
(power_CMonoid u k0 [#] power_CMonoid u l0))))->
M -> (C_as_CMonoid (Z_of_nat k)(Z_of_nat (l-k)) H2 H3).
Defined.
Lemma to_C_strext:
forall (M:CMonoid)(u:M)(k l:nat)(H2:((Z_of_nat (l-k))>0)%Z)
(H3:((Z_of_nat k)>=0)%Z)(H:(is_generator M u))(H1:(k<l and
(power_CMonoid u k [=] power_CMonoid u l)
and ((forall (k0 l0:nat), (k0<>l0 and (k0<k or (k0=k and l0<l)))->
(power_CMonoid u k0 [#] power_CMonoid u l0))))),
(fun_strext (to_C M u k l H2 H3 H H1)):CProp.
Definition to_C_as_csf (M:CMonoid)(u:M)(k l:nat)
(H2: ((Z_of_nat (l-k))>0)%Z)(H3:((Z_of_nat k)>=0)%Z)(H:(is_generator M u))
(H1:(k<l and
(power_CMonoid u k [=] power_CMonoid u l)
and ((forall (k0 l0:nat), k0<>l0 and (k0<k or (k0=k and l0<l))->
(power_CMonoid u k0 [#] power_CMonoid u l0)))))
:=
(Build_CSetoid_fun M (C_as_CMonoid k (l - k)%nat H2 H3)
(to_C M u k l H2 H3 H H1) (to_C_strext M u k l H2 H3 H H1)).
Lemma mod_nat_pi:forall (k l i:nat)(H:(k>0)%Z)(H0:(l>0)%Z),
k=l -> (mod_nat i k H)=(mod_nat i l H0).
Section Char.
Variable M:CMonoid.
Variable k l:nat.
Variable H3: k>=0.
Variable H5: l-k>0.
Variable c0: cs_crr (csg_crr (cm_crr M)).
Variable power_mod:forall (k l n : N) (H2 : (Z_of_nat (l - k) > 0)%Z),
k < n ->
k < l
and power_CMonoid c0 k[=]power_CMonoid c0 l
and (forall k0 l0 : N, k0<>l0 and
(k0 < k or k0 = k and l0 < l) ->
power_CMonoid c0 k0[#]power_CMonoid c0 l0) ->
power_CMonoid c0 n[=]
power_CMonoid c0 (k + mod_nat (n - k) (l - k) H2).
Variable w_inj:forall k l a b : N,
a < l ->
b < l ->
k < l
and power_CMonoid c0 k[=]power_CMonoid c0 l
and (forall k0 l0 : N, k0<>l0 and
(k0 < k or k0 = k and l0 < l) ->
power_CMonoid c0 k0[#]power_CMonoid c0 l0) ->
power_CMonoid c0 a[=]power_CMonoid c0 b -> a = b.
Variable smallest: k < l
and power_CMonoid c0 k[=]power_CMonoid c0 l
and (forall k0 l0 : N, k0<>l0 and
(k0 < k or k0 = k and l0 < l) ->
power_CMonoid c0 k0[#]power_CMonoid c0 l0).
Variable n0 n1 n2:nat.
Variable a b:cs_crr (csg_crr (cm_crr M)).
Variable Hn0:power_CMonoid c0 n0[=]
csbf_fun (csg_crr (cm_crr M)) (csg_crr (cm_crr M))
(csg_crr (cm_crr M)) (csg_op (c:=cm_crr M)) a b.
Variable Hn1:power_CMonoid c0 n1[=]a.
Variable Hn2: power_CMonoid c0 n2[=]b.
Lemma Char1:(k + (n1 - k)%nat mod (l - k)%nat + (k + (n2 - k)%nat mod (l - k)%nat) <
k + (l - k)%nat)%Z->l<=n1 -> l<= n0 -> l<=n2 ->
(k + (n1 - k)%nat mod (l - k)%nat + (k + (n2 - k)%nat mod (l - k)%nat))%Z =
(k + (n0 - k)%nat mod (l - k)%nat)%Z.
Lemma Char2:(Z_of_nat k + Z_of_nat (l - k) <=
Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) +
(Z_of_nat k + Z_of_nat (n2 - k) mod Z_of_nat (l - k)))%Z ->
l<=n1-> l<=n2 -> l<=n0->
(Z_of_nat k +
(Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) +
(Z_of_nat k + Z_of_nat (n2 - k) mod Z_of_nat (l - k)) -
Z_of_nat k) mod Z_of_nat (l - k))%Z =
(Z_of_nat k + Z_of_nat (n0 - k) mod Z_of_nat (l - k))%Z.
Lemma Char3:(Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) + Z_of_nat n2 <
Z_of_nat k + Z_of_nat (l - k))%Z ->
n2 < l ->
l <= n1 ->
l <= n0 ->
(Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) + Z_of_nat n2)%Z =
(Z_of_nat k + Z_of_nat (n0 - k) mod Z_of_nat (l - k))%Z.
Lemma Char4:(Z_of_nat k + Z_of_nat (l - k) <=
Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) + Z_of_nat n2)%Z ->
n2 < l ->
l <= n1 ->
l <= n0 ->
(Z_of_nat k +
(Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) + Z_of_nat n2 -
Z_of_nat k) mod Z_of_nat (l - k))%Z =
(Z_of_nat k + Z_of_nat (n0 - k) mod Z_of_nat (l - k))%Z.
Lemma Char5:(Z_of_nat n1 + Z_of_nat n2 < Z_of_nat k + Z_of_nat (l - k))%Z ->
n2 < l ->
power_CMonoid c0 n2[=]b ->
n1 < l ->
l <= n0 ->
(Z_of_nat n1 + Z_of_nat n2)%Z =
(Z_of_nat k + Z_of_nat (n0 - k) mod Z_of_nat (l - k))%Z.
Lemma Char6:(Z_of_nat k + Z_of_nat (l - k) <= Z_of_nat n1 + Z_of_nat n2)%Z ->
n2 < l ->
power_CMonoid c0 n2[=]b ->
n1 < l ->
l <= n0 ->
(Z_of_nat k + (Z_of_nat n1 + Z_of_nat n2 - Z_of_nat k) mod Z_of_nat (l - k))%Z =
(Z_of_nat k + Z_of_nat (n0 - k) mod Z_of_nat (l - k))%Z.
Lemma Char7: (Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) +
(Z_of_nat k + Z_of_nat (n2 - k) mod Z_of_nat (l - k)) <
Z_of_nat k + Z_of_nat (l - k))%Z ->
l <= n2 ->
power_CMonoid c0 n2[=]b ->
l <= n1 ->
power_CMonoid c0 n1[=]a ->
n0 < l ->
(Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) +
(Z_of_nat k + Z_of_nat (n2 - k) mod Z_of_nat (l - k)))%Z =
Z_of_nat n0.
Lemma Char8: (Z_of_nat k + Z_of_nat (l - k) <=
Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) +
(Z_of_nat k + Z_of_nat (n2 - k) mod Z_of_nat (l - k)))%Z ->
l <= n2 ->
power_CMonoid c0 n2[=]b ->
l <= n1 ->
power_CMonoid c0 n1[=]a ->
n0 < l ->
(Z_of_nat k +
(Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) +
(Z_of_nat k + Z_of_nat (n2 - k) mod Z_of_nat (l - k)) -
Z_of_nat k) mod Z_of_nat (l - k))%Z = Z_of_nat n0.
Lemma Char9: (Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) + Z_of_nat n2 <
Z_of_nat k + Z_of_nat (l - k))%Z ->
n2 < l ->
power_CMonoid c0 n2[=]b ->
l <= n1 ->
power_CMonoid c0 n1[=]a ->
n0 < l ->
(Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) + Z_of_nat n2)%Z =
Z_of_nat n0.
Lemma Char10:(Z_of_nat k + Z_of_nat (l - k) <=
Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) + Z_of_nat n2)%Z ->
n2 < l ->
power_CMonoid c0 n2[=]b ->
l <= n1 ->
power_CMonoid c0 n1[=]a ->
n0 < l ->
(Z_of_nat k +
(Z_of_nat k + Z_of_nat (n1 - k) mod Z_of_nat (l - k) + Z_of_nat n2 -
Z_of_nat k) mod Z_of_nat (l - k))%Z = Z_of_nat n0.
Lemma Char11:(Z_of_nat n1 + Z_of_nat n2 < Z_of_nat k + Z_of_nat (l - k))%Z ->
n2 < l ->
power_CMonoid c0 n2[=]b ->
n1 < l ->
power_CMonoid c0 n1[=]a ->
n0 < l -> (Z_of_nat n1 + Z_of_nat n2)%Z = Z_of_nat n0.
Lemma Char12:(Z_of_nat k + Z_of_nat (l - k) <= Z_of_nat n1 + Z_of_nat n2)%Z ->
n2 < l ->
power_CMonoid c0 n2[=]b ->
n1 < l ->
power_CMonoid c0 n1[=]a ->
n0 < l ->
(Z_of_nat k + (Z_of_nat n1 + Z_of_nat n2 - Z_of_nat k) mod Z_of_nat (l - k))%Z =
Z_of_nat n0.
End Char.
Section MP.
Variable M:CMonoid.
Variable u:M.
Variable gen:(is_generator M u).
Variable k l:nat.
Variable smallest: k < l
and power_CMonoid u k[=]
power_CMonoid u l
and (forall k0 l0 : N, k0<>l0 and
(k0 < k or k0 = k and l0 < l) ->
power_CMonoid u k0[#]
power_CMonoid u l0).
Variable a b:cs_crr (csg_crr (cm_crr M)).
Variable H3: k >= 0.
Let H4:=(inj_ge k 0 H3 ).
Variable H7:((l - k)%nat > 0)%Z.
Variable H5: l - k > 0.
Let H6:=(inj_gt (l - k) 0 H5 ).
Lemma pres_mult:(
csf_fun M (C_as_CMonoid k (l - k)%nat H6 H4)
(to_C_as_csf M u k l H7 H4 gen smallest) (csbf_fun M M M (csg_op (c:=M)) a b)[=]
csbf_fun (C_as_CMonoid k (l - k)%nat H6 H4)
(C_as_CMonoid k (l - k)%nat H6 H4) (C_as_CMonoid k (l - k)%nat H6 H4)
(csg_op (c:=C_as_CMonoid k (l - k)%nat H6 H4))
(csf_fun M (C_as_CMonoid k (l - k)%nat H6 H4)
(to_C_as_csf M u k l H7 H4 gen smallest ) a)
(csf_fun M (C_as_CMonoid k (l - k)%nat H6 H4)
(to_C_as_csf M u k l H7 H4 gen smallest ) b)).
End MP.
Section ZP.
Variable M:CMonoid.
Variable u:M.
Variable gen: (is_generator M u).
Variable l k: N.
Variable smallest:k < l
and power_CMonoid u k[=]
power_CMonoid u l
and (forall k0 l0 : N, k0<>l0 and
(k0 < k or k0 = k and l0 < l) ->
power_CMonoid u k0[#]
power_CMonoid u l0).
Variable H3:k >= 0.
Let H4:=(inj_ge k 0 H3).
Variable H7:((l - k)%nat > 0)%Z.
Variable H5: l - k > 0.
Let H6:= (inj_gt (l - k) 0 H5).
Lemma pres_zero:csf_fun M (C_as_CMonoid k (l - k)%nat H6 H4)
(to_C_as_csf M u k l H7 H4 gen smallest ) 0[=]0.
End ZP.
Section inj_surj.
Variable M:CMonoid.
Variable u:M.
Variable gen: (is_generator M u).
Variable k l:nat.
Variable smallest:k < l
and power_CMonoid u k[=]
power_CMonoid u l
and (forall k0 l0 : N,k0<>l0 and
(k0 < k or k0 = k and l0 < l) ->
power_CMonoid u k0[#]
power_CMonoid u l0).
Variable H7:((l - k)%nat > 0)%Z.
Variable H4: (k >= 0)%Z.
Section IL.
Variable a0 : M.
Variable a1 : M.
Variable ap : a0[#]a1.
Variable H1 : k < l.
Variable power_mod : forall (n : N) (H2 : (Z_of_nat (l - k) > 0)%Z),
k < n ->
k < l
and power_CMonoid u k[=]power_CMonoid u l
and ((forall k0 l0 : N, k0<>l0 and
(k0 < k or k0 = k and l0 < l) ->
power_CMonoid u k0[#]power_CMonoid u l0):CProp) ->
power_CMonoid u n[=]
power_CMonoid u (k + mod_nat (n - k) (l - k) H2).
Lemma power_inj: forall (n0 n1:nat),
(power_CMonoid u n0[#]power_CMonoid u n1)-> n0<>n1.
Lemma to_C_inj1:forall(n0 : N)
(Hn0 : power_CMonoid u n0[=]a0)
(n1 : N),
l <= n1 ->
power_CMonoid u n1[=]a1 ->
l <= n0 ->
(k + (n1 - k)%nat mod (l - k)%nat)%Z <>
(k + (n0 - k)%nat mod (l - k)%nat)%Z.
Lemma to_C_inj2:forall(n0 : N)
(Hn0 : power_CMonoid u n0[=]a0)
(n1 : N), n1 < l ->
power_CMonoid u n1[=]a1 ->
l <= n0 ->
Z_of_nat n1 <> (Z_of_nat k + Z_of_nat (n0 - k) mod Z_of_nat (l - k))%Z.
End IL.
Lemma to_C_inj:injective (to_C_as_csf M u k l H7 H4 gen smallest).
Lemma to_C_surj:surjective (to_C_as_csf M u k l H7 H4 gen smallest).
End inj_surj.
Definition cyc_to_nat: forall (M:CMonoid)(u:M),
(is_generator M u)->M->nat_as_CMonoid.
Defined.
Section CTN.
Variable M:CMonoid.
Variable u:M.
Variable gen:(is_generator M u).
Lemma cyc_to_nat_strext: (((forall (k l:nat),k<l->
(power_CMonoid u k [#] power_CMonoid u l))
:CProp)
->
(fun_strext (cyc_to_nat M u gen)):CProp):CProp.
Definition cyc_to_nat_as_csf
(H0:(forall (k l:nat),k<l->(power_CMonoid u k [#] power_CMonoid u l))):=
(Build_CSetoid_fun M nat_as_CMonoid (cyc_to_nat M u gen) (cyc_to_nat_strext H0)).
Lemma weakly_inj2:forall (a b:nat),
(forall (k l:nat),k<l->(power_CMonoid u k [#] power_CMonoid u l))
->
(power_CMonoid u a[=]power_CMonoid u b )->
a = b.
End CTN.
Section Th17.
Variable M:CMonoid.
Variable u:M.
Variable gen:(is_generator M u).
Theorem Th17_partI:
({k:nat | {l:nat |k<l and (power_CMonoid u k [=] power_CMonoid u l)
and (forall (k0 l0:nat), k0<>l0 and (k0<k or (k0=k and l0<l))->
(power_CMonoid u k0 [#] power_CMonoid u l0) )}}
->
{k:Z|{H0:(k>=0)%Z|{n:Z|{H:(n>0)%Z| (isomorphic M (C_as_CMonoid k n H H0))}}}}):
CProp.
Theorem Th17_partII:
(((forall (k l:nat),k<l->
(power_CMonoid u k [#] power_CMonoid u l))
:CProp)
->(isomorphic M nat_as_CMonoid)):CProp.
End Th17.
Definition plus_nminus1:forall (n:Z)(H:(n>0)%Z)(H0:(0>=0)%Z),
(CSetoid_un_op (C_as_CMonoid 0%Z n H H0)).
Defined.
Definition c_n_minus_a:forall (n:Z)(H:(n>0)%Z)(H0:(0>=0)%Z)(a:(C_as_CMonoid 0%Z n H H0)),
(C_as_CMonoid 0%Z n H H0).
Defined.
Lemma C_0_n:(forall (n:Z)(H:(n>0)%Z)(H0:(0>=0)%Z)(a:(C_as_CMonoid 0%Z n H H0)),
(invertible (C_as_CMonoid 0%Z n H H0) a)):CProp.
Lemma not_inv:
forall (n k:Z)(H:(k>0)%Z)(H0:(n>0)%Z)
(a:(C_as_CMonoid k%Z n H0 (Zgt_Zge k 0 H))),
a[#](@cm_unit (C_as_CMonoid k%Z n H0 (Zgt_Zge k 0 H)))->
~ (invertible (C_as_CMonoid k%Z n H0 (Zgt_Zge k 0 H)) a).
Lemma unit_inv:
(forall (n k:Z)(H:(k>=0)%Z)(H0:(n>0)%Z),
(invertible (C_as_CMonoid k%Z n H0 H) (@cm_unit (C_as_CMonoid k%Z n H0 H)))):
CProp.