proposition: Lemma sK_it : forall tup : Knes_tup, AbsCC (Knes_fun tup[-]tup) [^]n [<=] c_el tup.
proof: Proof. intro tup. generalize (Ktpp_prop tup (Knes_fun tup)). auto. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)