proposition: Lemma fusc_quo_numden n (q := fusc_quo n): natp n -> Qnum q = (fuscz n) /\ Qden q = (fuscz (csucc n)).
proof: Proof. move => nN. move:(fusc_coprime nN). have: inc (fuscz (csucc n)) BZps. apply/BZps_iP; split; first exact:(BZ_of_natp_i (NS_fusc (NS_succ nN))). by move => /pr1_def; apply:fusc_nz'. apply: (BQdiv_numden1 (BZ_of_nat_i (NS_fusc nN))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)