proposition: Lemma ceilP (r : R) : r <= IZR (ceil r) < r + 1.
proof: Proof. rewrite /ceil; case: ifPn => [|] /eqP r0. rewrite frac_Int_part //; Lra.lra. case: (floorP r); rewrite /floor => H1 /Rle_lt_or_eq_dec[] H2. rewrite up_Int_part plus_IZR; Lra.lra. by exfalso; apply/r0; rewrite subR_eq0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)