proposition: Lemma floor_sum (a:rat) (b: int): floorq (a + b%:Q) = floorq a + b.
proof: Proof. symmetry; apply:floorp2; case/andP:(floorp1 a) => [l1 l2]. by rewrite intrD lerD2r l1 addrAC ltrD2r l2. 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)