proposition: Lemma continuous_neq_0 : forall (f:R -> R) (x0:R), continuity_pt f x0 -> f x0 <> 0 -> exists eps : posreal, (forall h:R, Rabs h < eps -> f (x0 + h) <> 0).
proof: Proof. intros; unfold continuity_pt in H; unfold continue_in in H; unfold limit1_in in H; unfold limit_in in H; elim (H (Rabs (f x0 / 2))). 2:{ change (0 < Rabs (f x0 / 2)). apply Rabs_pos_lt; unfold Rdiv; apply prod_neq_R0;lra. } intros; elim H1; intros. exists (mkposreal x H2). intros; assert (H5 := H3 (x0 + h)). cut (dist R_met (x0 + h) x0 < x -> dist R_met (f (x0 + h)) (f x0) < Rabs (f x0 / 2)). 2:{ assert (H6 := Req_dec x0 (x0 + h)); elim H6; intro. - intro; rewrite <- H7. unfold R_met, dist; unfold Rdist; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rabs_pos_lt. unfold Rdiv; apply prod_neq_R0; [ assumption | apply Rinv_neq_0_compat; discrR ]. - intro; apply H5. split. + unfold D_x, no_cond. split; trivial || assumption. + assumption. } unfold dist; simpl; unfold Rdist; replace (x0 + h - x0) with h by ring. intros; assert (H7 := H6 H4). red; intro. rewrite H8 in H7; unfold Rminus in H7; rewrite Rplus_0_l in H7; rewrite Rabs_Ropp in H7; unfold Rdiv in H7; rewrite Rabs_mult in H7; pattern (Rabs (f x0)) at 1 in H7; rewrite <- Rmult_1_r in H7. assert (0 < Rabs (f x0)) by (apply (Rabs_pos_lt _ H0)). assert (H10 := Rmult_lt_reg_l _ _ _ H9 H7). assert (Rabs (/ 2) = / 2) by (apply Rabs_pos_eq;lra). assert (Hyp : 0 < 2) by prove_sup0. rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10); rewrite Rmult_1_r in H12; rewrite Rinv_r in H12; [ idtac | discrR ]. now apply lt_IZR in H12. Qed.
imports: Rbase Rfunctions Ranalysis1 Lra