proposition: Lemma Exercise5_9h q n k: natp n -> natp q -> natp k -> k <=c n -> \0c <c q -> (Ex59b_num q n k) = (Ex59b_den q n k) *c ((binom (Ex59b_num1 q n k) k) *c (Ex59_val q (n -c k))).
proof: Proof. move => nN qN kN sa sb. move:(Exercise5_9g nN qN kN) => [ha hb hx hd he]. have sb': \1c <=c q by apply/cge1P. have hf:=(cdiff_pr sa). have hf':=(cdiff_pr sb'). move:(NS_diff k nN)(NS_diff \1c qN) => n'N q'N. have ea: Ex59b_num1 q n k = (n -c k) *c q +c k. rewrite /Ex59b_num1 -{1} hf -{1 3} hf'. rewrite cprodDl (cprod1l (CS_sum2 _ _)) !cprodDr (cprod1r (CS_nat n'N)). have ra:=(NS_sum nN (NS_prod q'N n'N)). rewrite(cprodC _ k)(csumC (k *c _)) csumA hf (cdiff_pr1 ra (NS_prod kN q'N)). by rewrite (csumC _ k) cprodC csumA hf. have ea': Ex59b_num1 q n k -c k = (n -c k) *c q. by rewrite ea (cdiff_pr1 (NS_prod n'N qN) kN). have hg: (k <=c Ex59b_num1 q n k) by rewrite ea; apply:(Nsum_Mle0 _ kN). rewrite /Ex59b_num /Ex59b_den - (binom_good ha kN hg) ea' (cprodC _ q). rewrite -/(Ex59_num q (n -c k)) (Exercise5_9c' n'N qN sb). rewrite /Ex59_den - (cprodA (factorial k)). set b := _ *c _ ^c _. rewrite (cprodC _ b). set a := binom _ _;set c := factorial _. by rewrite cprodACA cprodA (cprodC a). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)