proposition: Lemma rat_in_PP x: reflect (exists n, x = n.+1%:Z%:Q) (rat_in_P x).
proof: Proof. apply:(iffP idP) => [h | [n ->]]; last by apply:rat_in_P_nat. by move/andP:h => [/eqP {2} -> /eqP ha]; exists `|floorq x|.-1; rewrite - ha. 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)