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