proposition: Lemma g_not_zero2 : forall g a b, b > a -> limit_div_neg g (open_interval a b) a -> exists a', open_interval a b a' /\ forall x, open_interval a a' x -> g x <> 0.
proof: Proof. intros g a b Hab Zg. unfold limit_div_neg in Zg. assert (1 > 0) by lra. specialize (Zg 1 H). destruct Zg as [alp [Halp H3]]. exists (a + Rmin ((b - a) / 2) (alp / 2)). assert (H6 : alp / 2 > 0) by lra. assert ((b - a) > 0) by lra. assert ((b-a) /2 > 0). apply (Rmult_gt_0_compat (/2)) in H0. now lra. now lra. split. unfold open_interval. split. assert (Rmin ((b-a) /2) (alp / 2) > 0). now apply Rmin_glb_lt; assumption. now lra. apply Rle_lt_trans with (a + (b-a) /2). apply Rplus_le_compat_l. now apply Rmin_l. assert (b - a - (b-a) /2 > 0). field_simplify. now lra. now lra. intros. unfold open_interval in H0. assert (g x < - 1). apply H3. unfold open_interval. unfold open_interval in H2. split. now apply H2. apply Rlt_trans with (a + Rmin ((b-a)/2) (alp /2)). now apply H2. apply Rle_lt_trans with (a + (b-a) /2). apply Rplus_le_compat_l. now apply Rmin_l. assert (b - a - (b-a) /2 > 0). field_simplify. now lra. now lra. unfold R_dist. unfold open_interval in H2. destruct H2. apply Rlt_trans with (alp/2). apply Rlt_le_trans with (Rmin ((b-a) / 2) (alp /2)). now rewrite Rabs_right; lra. now apply Rmin_r. now lra. intro. lra. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality