proposition: Lemma floorQ_unique (r : rat) (m : int) : m%:Q <= r < (m + 1)%:Q -> m = floorQ r.
proof: Proof. have /andP[Hfloor1 Hfloor2] := floorQ_spec r. case/andP => Hm1 Hm2. move: (le_lt_trans Hm1 Hfloor2) (le_lt_trans Hfloor1 Hm2). rewrite -[n in _ + n]rat1 -intrD !ltr_int !ltzD1 => ? ?. by apply/eqP; rewrite eq_le; apply/andP. Qed.
imports: mathcomp(all_ssreflect all_algebra)