proposition: Lemma sK_c0 : forall i : nat, c_el (Knes_fun_it i) [=] qK[^]i[*]c0.
proof: Proof. simple induction i. simpl in |- *. rational. intros. simpl in |- *. generalize (sK_c (Knes_fun_it n0)). intro H1. apply eq_transitive_unfolded with (qK[*]c_el (Knes_fun_it n0)). assumption. rstepr (qK[*] (nexp IR n0 qK[*]c0)). apply mult_wdr. exact H. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)