proposition: Lemma sK_c : forall tup : Knes_tup, c_el (Knes_fun tup) [=] qK[*]c_el tup.
proof: Proof. intro tup. generalize (Ktp_prop tup (Knes_fun tup)). auto. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)