proposition: Lemma rat_in_NP x: reflect (exists n, x = n%:Z%:Q) (rat_in_N x).
proof: Proof. apply:(iffP idP) => [h | [n ->]]; last by apply:rat_in_N_nat. by move/andP:h => [/eqP {2} -> /int_in_NP [n ->]]; exists n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)