proposition: Lemma ceilD : {in int_num & Rreal, {morph ceil : x y / x + y}}.
proof: Proof. move=> _ y /intrP[m ->] Ry; apply: ceil_def. by rewrite -addrA 3!rmorphD /= intrKceil lerD2l ltrD2l -rmorphD ceil_itv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)