proposition: Lemma floorQ_grows (r1 r2 : rat) : r1 <= r2 -> floorQ r1 <= floorQ r2.
proof: Proof. move => Hr12. suff: (floorQ r1)%:Q < (floorQ r2 + 1)%:Q by rewrite ltr_int ltzD1. rewrite intrD; case/andP: (floorQ_spec r2) => _; apply: le_lt_trans. by apply: le_trans Hr12; case/andP: (floorQ_spec r1). Qed.
imports: mathcomp(all_ssreflect all_algebra)