proposition: Lemma Exercise5_9g q n k: natp n -> natp q -> natp k -> [/\ natp(Ex59b_num1 q n k), natp(Ex59b_num q n k), natp (Ex59b_den q n k), natp(Ex59b_val q n k) & (Ex59b_den q n k) <> \0c].
proof: Proof. move => nN qN kN. have pa: natp (Ex59b_num1 q n k) by apply: NS_diff; apply:(NS_prod qN nN). have pb: natp (Ex59b_num q n k) by apply: NS_factorial. have pc: natp (n -c k) by apply: NS_diff. have pd: natp (Ex59b_den q n k). apply:NS_prod; first by apply:NS_prod; apply:NS_factorial. apply:(NS_pow (NS_factorial qN) pc). have pe:Ex59b_den q n k <> \0c. apply:cprod2_nz; first by apply:cprod2_nz; apply:factorial_nz. by apply:cpow_nz;apply:factorial_nz. by split => //; apply:NS_quo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)