proposition: Lemma floorp2 x (y: int): y%:Q <= x < y%:Q +1 -> y = floorq x.
proof: Proof. move: (floorp1 x) => /andP [sa sb] /andP [sc sd]. apply/eqP; rewrite Order.POrderTheory.eq_le - !ltzD1 -! (ltr_int rat). by rewrite - !succq (Order.POrderTheory.le_lt_trans sc sb) (Order.POrderTheory.le_lt_trans sa sd). 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)