proposition: Lemma Exercise5_9b' q n: natp n -> natp q -> (Ex59_den q n) <> \0c.
proof: Proof. move => nN qN; apply:(cprod2_nz (factorial_nz nN)). exact:(cpow_nz (factorial_nz qN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)