proposition: Lemma sK_prop1 : forall i : nat, AbsCC p ! (sK i) [<=] qK[^]i[*]c0.
proof: Proof. unfold sK in |- *. simple induction i. simpl in |- *. rstepr c0. apply less_leEq; exact p0ltc0. intros. simpl in |- *. generalize (Kt_prop (Knes_fun (Knes_fun_it n0))). intro H2. apply leEq_wdr with (c_el (Knes_fun (Knes_fun_it n0))). apply less_leEq; assumption. generalize (sK_c (Knes_fun_it n0)). intro H3. eapply eq_transitive_unfolded. apply H3. generalize (sK_c0 n0). intro H4. rstepr (qK[*] (nexp IR n0 qK[*]c0)). apply mult_wdr. exact H4. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)