proposition: Lemma narrow_interval_lower_bound a b x : a > 0 -> a * x >= b -> x >= ceiling b a.
proof: Proof. rewrite !Z.ge_le_iff. unfold ceiling. intros Ha H. generalize (Z_div_mod b a Ha). destruct (Z.div_eucl b a) as (q,r). intros (->,(H1,H2)). destruct r as [|r|r]. - rewrite Z.add_0_r in H. apply Z.mul_le_mono_pos_l in H; auto with zarith. - assert (0 < Z.pos r) by easy. rewrite Z.add_1_r, Z.le_succ_l. apply Z.mul_lt_mono_pos_l with a. + auto using Z.gt_lt. + eapply Z.lt_le_trans. 2: eassumption. now apply Z.lt_add_pos_r. - now elim H1. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory