proposition: Lemma Exercise5_9b q n: natp n -> natp q -> [/\ natp(Ex59_num q n), natp(Ex59_den q n) & natp (Ex59_val q n) ].
proof: Proof. move => nN qN. have ha :=(NS_factorial (NS_prod qN nN)). have hb := (NS_prod (NS_factorial nN) (NS_pow (NS_factorial qN) nN)). by split => //; apply: NS_quo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)