proposition: Lemma sK_prop2 : forall i : nat, AbsCC (sK (S i) [-]sK i) [^]n [<=] qK[^]i[*]c0.
proof: Proof. unfold sK in |- *. simpl in |- *. intro i. generalize (sK_it (Knes_fun_it i)). intro H0. eapply leEq_wdr. apply H0. exact (sK_c0 i). Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)