proposition: Lemma floor_addEpsilon (m : int) (epsilon : rat) : 0 <= epsilon < 1 -> floorQ (m%:Q + epsilon) = m.
proof: Proof. move=> /andP[Heps1 Heps2]. by apply/esym/floorQ_unique; rewrite lerDl Heps1 intrD ltrD2l. Qed.
imports: mathcomp(all_ssreflect all_algebra)