proposition: Lemma Rint_ltr_addr1 (x y : R) : x \is a Rint -> y \is a Rint -> (x < y + 1) = (x <= y).
proof: Proof. move=> /RintP[xi ->] /RintP[yi ->]; rewrite -{3}[1]mulr1z. by rewrite -intrD !(ltr_int, ler_int) ltzD1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid