proposition: Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}.
proof: Proof. by move=> x y ?; rewrite lerNl opprK le_Rfloor // lerNl opprK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid