proposition: Lemma floor_div (a b:int): 0 < b -> floorq (a%:Q / b%:Q) = (a %/b)%Z.
proof: Proof. rewrite /floorq; case: divqP => // k x _;rewrite (pmulr_lgt0 _ (denq_gt0 x)). by move => h;rewrite divzMpl. 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)