proposition: Lemma Exercise5_9k5 n q k J (e:= nth_elt J) (e' := fun i => e i -c q *c i) (T := functions_incr_nat k (csucc (q *c (n -c k)))): natp q -> natp n -> k <=c n -> Ex59_Jprop q n k J -> inc (Lf e' k (csucc (q *c (n -c k)))) T /\ cardinal T = binom ((q *c (n -c k)) +c k) k.
proof: Proof. move => qN nN lkn h. have kN := NS_le_nat lkn nN. have tN:=(NS_prod qN (NS_diff k nN)). split; last by apply: card_increasing_nat. move:(Exercise5_9k4 qN nN lkn h) => [sa sb sc sd]. set f := Lf _ _ _. have ax:lf_axiom e' k (csucc (q *c (n -c k))). move => x /(NltP kN) lxk. move:(sa _ lxk) NS0 (sd _ lxk) => eN zN es. by apply/(NleP tN). have fa: inc f (functions k (csucc (q *c (n -c k)))). by apply/functionsP;rewrite/f; saw; apply:lf_function. apply/(increasing_nat_prop kN (NS_succ tN)); split => //. move =>x y lxy lyk. have xI: inc x k by apply/(NltP kN); exact(cle_ltT lxy lyk). have yI: inc y k by apply/(NltP kN). rewrite /f !LfV//; apply:(sc _ _ lxy lyk). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)