proposition: Lemma Exercise5_9c' q n: natp n -> natp q -> \0c <c q -> (Ex59_num q n) = (Ex59_val q n) *c (Ex59_den q n).
proof: Proof. move => nN qN qp. by rewrite (cdivides_pr (Exercise5_9c nN qN qp)) cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)