proposition: Lemma Exercise5_9d q n: natp n -> natp q -> \0c <c q -> (Ex59_val q n) <> \0c.
proof: Proof. move => nN qN qp dz. move:(Exercise5_9c' nN qN qp). rewrite dz cprod0l. apply: (factorial_nz (NS_prod qN nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)