proposition: Lemma g_a_zero : g a = 0.
proof: Proof. assert (forall x (Hclose : a <= x <= b), continuity_pt g x). intros. apply Cg. now apply Hclose. unfold continuity_pt in H. unfold continue_in in H. specialize (H a). assert (a <= a <= b) by intuition. apply H in H0. apply (limit_open g a b) in H0. eapply single_limit; [ | apply H0 | apply Zg ]. unfold adhDa. intros. 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 H2. now lra. now lra. split. unfold open_interval. split. assert (Rmin ((b - a) /2) (alp/2) > 0). apply Rmin_Rgt_r. now intuition. now lra. apply Rle_lt_trans with (a + (b-a) / 2). apply Rplus_le_compat. now intuition. now apply Rmin_l. assert (b - a - (b - a) / 2 > 0). field_simplify. now lra. now lra. unfold R_dist. rewrite Rabs_right. ring_simplify. apply Rle_lt_trans with (alp / 2). now apply Rmin_r. now lra. ring_simplify. apply Rle_ge. apply Rmin_glb; intuition. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality