proposition: Lemma limit_div_pos_open : forall a b b' f, open_interval a b b' -> limit_div_pos f (open_interval a b') a -> limit_div_pos f (open_interval a b) a.
proof: Proof. intros. unfold limit_div_pos in *. intros m Hm. destruct (H0 m Hm) as [alp [Halp Hsolve]]. exists (Rmin alp (b' - a)). split. apply Rmin_Rgt_r. split; destruct H; lra. intros. assert (x < b'). unfold R_dist in H2. rewrite Rabs_right in H2. replace b' with ((b' - a) + a) by ring. assert (x - a < b' - a). apply Rlt_le_trans with (Rmin alp (b'- a)). apply H2. apply Rmin_r. lra. destruct H1; lra. apply Hsolve. split. apply H1. apply H3. apply Rlt_le_trans with (Rmin alp (b'-a)). apply H2. apply Rmin_l. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality