proposition: Lemma ceil_le_int x n : x \is Rreal -> x <= n%:~R = (ceil x <= n).
proof: Proof. rewrite -realN; move=> /(floor_ge_int (- n)). by rewrite mulrNz lerNl opprK => ->; rewrite lerNl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)