proposition: Lemma Exercise5_9h' q n k: natp n -> natp q -> natp k -> k <=c n -> \0c <c q -> (Ex59b_val q n k) = (binom (Ex59b_num1 q n k) k) *c (Ex59_val q (n -c k)).
proof: Proof. move => nN qN kN lkn qp. move: (Exercise5_9g nN qN kN) => [ha hb hc hd he]. have hf:=(proj33 (Exercise5_9b (NS_diff k nN) qN)). rewrite /Ex59b_val (Exercise5_9h nN qN kN lkn qp). by rewrite (cdivides_pr4 hc (NS_prod (NS_binom ha kN) hf) he). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)