proposition: Lemma ceil_floor x : x \is Rreal -> ceil x = floor x + (~~ (x \is a int_num)).
proof: Proof. case Ix: (x \is a int_num) => Rx /=. by apply/eqP; rewrite addr0 eqr_oppLR floorN. apply/ceil_def; rewrite addrK; move: (floor_itv Rx). by rewrite le_eqVlt -intrEfloor Ix /= => /andP[-> /ltW]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)