proposition: Lemma new_bound : exists b', (forall x, open_interval a b' x -> g x <> 0) /\ open_interval a b b'.
proof: Proof. unfold limit_div_neg in Zg. assert (1 > 0) by lra. destruct (Zg 1 H) as [alp [Halp Hsolve]]. exists (Rmin (a + alp) ((b + a) / 2)). split. intros. specialize (Hsolve x). assert (H3 : open_interval a b x). split. apply H0. destruct H0. apply Rlt_le_trans with (Rmin (a + alp) ((b + a) / 2)). apply H1. apply Rle_trans with ((b + a)/ 2). apply Rmin_r. apply Rle_trans with ((b + b) /2). assert (b + a <= b + b) by lra. unfold Rdiv. apply Rmult_le_compat_r. lra. apply H2. apply Req_le. field. specialize (Hsolve H3). assert (R_dist x a < alp). destruct H0. assert (x < a + alp). apply Rlt_le_trans with (Rmin (a + alp) ((b + a) /2)). apply H1. apply Rmin_l. unfold R_dist. rewrite Rabs_right. lra. lra. specialize (Hsolve H1). intro. lra. split. apply Rmin_glb_lt. lra. apply Rle_lt_trans with ((a +a) / 2). apply Req_le. field. unfold Rdiv. apply Rmult_lt_compat_r. lra. intuition. apply Rle_lt_trans with ((b + a) / 2). apply Rmin_r. apply Rlt_le_trans with ((b + b) / 2). unfold Rdiv. apply Rmult_lt_compat_r. lra. intuition. apply Req_le. field. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality