proposition: Lemma Exercise5_9c q n: natp n -> natp q -> \0c <c q -> (Ex59_den q n) %|c (Ex59_num q n).
proof: Proof. move => nN qN qp. set E:= Nint (q *c n). have ce: cardinal E = q *c n by apply: (card_Nint (NS_prod qN nN)). rewrite -(partition_nq_pr9 nN qN qp ce) cprodC. apply:cdivides_pr1 (proj32 (Exercise5_9b nN qN)). apply: Exercise5_9a; apply/NatP; rewrite ce; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)