proposition: Lemma ceil_gt0 x : 0 < x -> 0 < ceil x.
proof: Proof. by move=> ?; rewrite /ceil oppr_gt0 floor_lt0 // ltrNl oppr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid