proposition: Lemma rat_in_ZP x: reflect (exists n, x = n%:Q) (rat_in_Z x).
proof: Proof. apply:(iffP idP) => [h | [n ->]]; first by exists (floorq x); apply/eqP. apply:rat_in_Z_int. 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)