proposition: Lemma power_k:forall (M:CMonoid)(u:M)(k l s:nat),(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)))):CProp)-> (power_CMonoid u k)[=](power_CMonoid u (k+(s*(l-k)))).
proof: Proof. intros M u k l s H. unfold is_generator in H. intros H0. induction s. simpl. replace (k+0) with k. intuition. intuition. simpl. replace (k+((l-k)+s*(l-k))) with (l + s*(l-k)). 2:intuition. set (H1:= (power_plus M u l (s*(l-k)))). astepr (csbf_fun (csg_crr (cm_crr M)) (csg_crr (cm_crr M)) (csg_crr (cm_crr M)) (csg_op (c:=cm_crr M)) (power_CMonoid u l) (power_CMonoid u (s * (l - k)))). elim H0. clear H0. intros H0 H0'. elim H0'. clear H0'. intros H0' H0''. cut ( power_CMonoid u l[=]power_CMonoid u k). intro H4. rewrite -> H4. 2: now apply eq_symmetric. set (H5:=(power_plus M u k (s*(l-k)))). cut (csbf_fun M M M (csg_op (c:=M)) (power_CMonoid u k) (power_CMonoid u (s * (l - k)))[=]power_CMonoid u (k + s * (l - k))). intros H6. now rewrite -> H6. now symmetry. 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