proposition: Lemma ceil_le0 x : x <= 0 -> ceil x <= 0.
proof: Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid