proposition: Lemma floorp1 x (y:= (floorq x)%:Q): y <= x < y+1.
proof: Proof. have ha: 0 < (denq x)%:Q by rewrite ltr0z (denq_gt0 x). rewrite -(divq_num_den x) ler_pdivlMr // succq ltr_pdivrMr //. rewrite - !rmorphM /= ler_int ltr_int lez_floor // ltz_ceil //. 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)