proposition: Lemma power_k_n:forall (M:CMonoid)(u:M)(k l n :nat) (H2:((Z_of_nat (l-k)>0)%Z)),(is_generator M u)->(k<n)-> ((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)))):CProp)-> (power_CMonoid u n)[=](power_CMonoid u (k+(mod_nat (n-k) (l-k) H2))).
proof: Proof. intros M u k l n H2 H H15. set (H13:=(power_k M u k l)). intros H4. set (H6:=(Z_div_mod_eq_full (n-k)(l-k))). cut (((n - k) mod (l - k))= (n-k)%Z -((l - k) * ((n - k) / (l - k))))%Z. 2:intuition. set (H7:=(mod_nat_correct (n-k) (l-k) H2)). intro H8. cut {s:nat | (mod_nat (n-k)(l-k) H2)=(n-k)-s*(l-k) and s*(l-k)<=(n-k)}. intro H9. elim H9. clear H9. intros s H9. elim H9. clear H9. intros H9 H9'. rewrite H9. replace (power_CMonoid u n) with (power_CMonoid u ((k+s*(l-k))+((n-k)-s*(l-k)))). 2: (replace ((k + s * (l - k))+((n - k) - s * (l - k))) with n). 2:reflexivity. rewrite -> (power_plus M u (k+(s*(l-k))) ((n-k)-s*(l-k))). rewrite -> (power_plus M u k (n-k-s*(l-k))). setoid_replace (power_CMonoid u (k + s * (l - k))) with (power_CMonoid u k). now reflexivity. unfold canonical_names.equiv. now intuition. cut (n=k+(n-k)). intro H10. cut (n=((k+(n-k))+(s*(l-k)-s*(l-k)))). intro H11. cut ((k+(n-k))+(s*(l-k)-s*(l-k)) = (k + s * (l - k) + (n - k - s * (l - k)))). intro H12. now rewrite<- H11 in H12. apply minus4. split. now intuition. exact H9'. rewrite<- H10. cut ((s*(l-k)-s*(l-k))=0). intro H11. rewrite H11. now intuition. now intuition. cut (n=n+(k-k)). intro H10. cut (n+(k-k)=k+(n-k)). intro H11. now rewrite<- H10 in H11. apply minus3. split; now intuition. cut ((k-k)=0). intro H10. now rewrite H10. now intuition. simpl. cut (l-k>0). intro H9. set (H10:=(quotient (l-k) H9 (n-k))). elim H10. clear H10. intros q H10. exists q. split. elim H10. clear H10. intros r H10'. elim H10'. clear H10'. intros H10' H10''. 3:intuition. cut ((n-k)= q*(l-k)+ (mod_nat (n-k)(l-k) H2)). intro H11. intuition. cut (r= (mod_nat (n-k)(l-k)H2)). intro H11. now rewrite<- H11. simpl. cut ((Z_of_nat r)=(mod_nat (n - k) (l - k) H2)). intro H11. intuition. rewrite<- H7. apply nat_Z_div with (n-k) q (l-k) ((Z_of_nat n - Z_of_nat k) / (Z_of_nat l - Z_of_nat k))%Z. exact H10'. intuition. cut (k<=l). intro H11. set (H12:=(inj_minus1 l k H11)). rewrite H12. cut (k<=n). intro H14. set (H16:=(inj_minus1 n k H14)). rewrite H16. exact H6. intuition. intuition. set (H17:=(Z_mod_lt (Z_of_nat (n-k)) (Z_of_nat (l-k)))). intuition. elim H10. clear H10. intros r H10. elim H10. clear H10. intros H10 H10'. intuition. Qed.
imports: Coq.Arith.Euclid CoRN.model.Zmod.Cmod CoRN.algebra.CSemiGroups CoRN.tactics.csetoid_rewrite CoRN.model.structures.Nsec CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms