proposition: Lemma cont_deriv : forall (f d:R -> R) (D:R -> Prop) (x0:R), D_in f d D x0 -> continue_in f D x0.
proof: Proof. unfold continue_in; unfold D_in; unfold limit1_in; unfold limit_in; unfold Rdiv; simpl; intros; elim (H eps H0); clear H; intros; elim H; clear H; intros; elim (Req_dec (d x0) 0); intro. - split with (Rmin 1 x); split. + elim (Rmin_Rgt 1 x 0); intros a b; apply (b (conj Rlt_0_1 H)). + intros; elim H3; clear H3; intros; generalize (let (H1, H2) := Rmin_Rgt 1 x (Rdist x1 x0) in H1); unfold Rgt; intro; elim (H5 H4); clear H5; intros; generalize (H1 x1 (conj H3 H6)); clear H1; intro; unfold D_x in H3; elim H3; intros. rewrite H2 in H1; unfold Rdist; unfold Rdist in H1; cut (Rabs (f x1 - f x0) < eps * Rabs (x1 - x0)). * intro; unfold Rdist in H5; generalize (Rmult_lt_compat_l eps (Rabs (x1 - x0)) 1 H0 H5); rewrite Rmult_1_r; intro; apply Rlt_trans with (r2 := eps * Rabs (x1 - x0)); assumption. * rewrite (Rminus_0_r ((f x1 - f x0) * / (x1 - x0))) in H1; rewrite Rabs_mult in H1; cut (x1 - x0 <> 0). -- intro; rewrite (Rabs_inv (x1 - x0)) in H1; generalize (Rmult_lt_compat_l (Rabs (x1 - x0)) (Rabs (f x1 - f x0) * / Rabs (x1 - x0)) eps (Rabs_pos_lt (x1 - x0) H9) H1); intro; rewrite Rmult_comm in H10; rewrite Rmult_assoc in H10; rewrite Rinv_l in H10. ++ rewrite Rmult_1_r in H10; rewrite Rmult_comm; assumption. ++ apply Rabs_no_R0; auto. -- apply Rminus_eq_contra; auto. - split with (Rmin (Rmin (/ 2) x) (eps * / Rabs (2 * d x0))); split. + cut (Rmin (/ 2) x > 0). * cut (eps * / Rabs (2 * d x0) > 0). -- intros; elim (Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) 0); intros a b; apply (b (conj H4 H3)). -- apply Rmult_gt_0_compat; auto. unfold Rgt; apply Rinv_0_lt_compat; apply Rabs_pos_lt; apply Rmult_integral_contrapositive; split. ++ discrR. ++ assumption. * elim (Rmin_Rgt (/ 2) x 0); intros a b; cut (0 < 2). -- intro; generalize (Rinv_0_lt_compat 2 H3); intro; fold (/ 2 > 0) in H4; apply (b (conj H4 H)). -- lra. + intros; elim H3; clear H3; intros; generalize (let (H1, H2) := Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) (Rdist x1 x0) in H1); unfold Rgt; intro; elim (H5 H4); clear H5; intros; generalize (let (H1, H2) := Rmin_Rgt (/ 2) x (Rdist x1 x0) in H1); unfold Rgt; intro; elim (H7 H5); clear H7; intros; clear H4 H5; generalize (H1 x1 (conj H3 H8)); clear H1; intro; unfold D_x in H3; elim H3; intros; generalize (not_eq_sym H5); clear H5; intro H5; generalize (Rminus_eq_contra x1 x0 H5); intro; generalize H1; pattern (d x0) at 1; rewrite <- (let (H1, H2) := Rmult_ne (d x0) in H2); rewrite <- (Rinv_l (x1 - x0) H9); unfold Rdist; unfold Rminus at 1; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))); rewrite (Rmult_comm (/ (x1 - x0) * (x1 - x0)) (d x0)); rewrite <- (Ropp_mult_distr_l_reverse (d x0) (/ (x1 - x0) * (x1 - x0))); rewrite (Rmult_comm (- d x0) (/ (x1 - x0) * (x1 - x0))); rewrite (Rmult_assoc (/ (x1 - x0)) (x1 - x0) (- d x0)); rewrite <- (Rmult_plus_distr_l (/ (x1 - x0)) (f x1 - f x0) ((x1 - x0) * - d x0)) ; rewrite (Rabs_mult (/ (x1 - x0)) (f x1 - f x0 + (x1 - x0) * - d x0)); clear H1; intro; generalize (Rmult_lt_compat_l (Rabs (x1 - x0)) (Rabs (/ (x1 - x0)) * Rabs (f x1 - f x0 + (x1 - x0) * - d x0)) eps (Rabs_pos_lt (x1 - x0) H9) H1); rewrite <- (Rmult_assoc (Rabs (x1 - x0)) (Rabs (/ (x1 - x0))) (Rabs (f x1 - f x0 + (x1 - x0) * - d x0))); rewrite (Rabs_inv (x1 - x0)); rewrite (Rinv_r (Rabs (x1 - x0)) (Rabs_no_R0 (x1 - x0) H9)); rewrite (let (H1, H2) := Rmult_ne (Rabs (f x1 - f x0 + (x1 - x0) * - d x0)) in H2) ; generalize (Rabs_triang_inv (f x1 - f x0) ((x1 - x0) * d x0)); intro; rewrite (Rmult_comm (x1 - x0) (- d x0)); rewrite (Ropp_mult_distr_l_reverse (d x0) (x1 - x0)); fold (f x1 - f x0 - d x0 * (x1 - x0)); rewrite (Rmult_comm (x1 - x0) (d x0)) in H10; clear H1; intro; generalize (Rle_lt_trans (Rabs (f x1 - f x0) - Rabs (d x0 * (x1 - x0))) (Rabs (f x1 - f x0 - d x0 * (x1 - x0))) (Rabs (x1 - x0) * eps) H10 H1); clear H1; intro; generalize (Rplus_lt_compat_l (Rabs (d x0 * (x1 - x0))) (Rabs (f x1 - f x0) - Rabs (d x0 * (x1 - x0))) ( Rabs (x1 - x0) * eps) H1); unfold Rminus at 2; rewrite (Rplus_comm (Rabs (f x1 - f x0)) (- Rabs (d x0 * (x1 - x0)))); rewrite <- (Rplus_assoc (Rabs (d x0 * (x1 - x0))) (- Rabs (d x0 * (x1 - x0))) (Rabs (f x1 - f x0))); rewrite (Rplus_opp_r (Rabs (d x0 * (x1 - x0)))); rewrite (let (H1, H2) := Rplus_ne (Rabs (f x1 - f x0)) in H2); clear H1; intro; cut (Rabs (d x0 * (x1 - x0)) + Rabs (x1 - x0) * eps < eps). * intro; apply (Rlt_trans (Rabs (f x1 - f x0)) (Rabs (d x0 * (x1 - x0)) + Rabs (x1 - x0) * eps) eps H1 H11). * clear H1 H5 H3 H10; generalize (Rabs_pos_lt (d x0) H2); intro; unfold Rgt in H0; generalize (Rmult_lt_compat_l eps (Rdist x1 x0) (/ 2) H0 H7); clear H7; intro; generalize (Rmult_lt_compat_l (Rabs (d x0)) (Rdist x1 x0) ( eps * / Rabs (2 * d x0)) H1 H6); clear H6; intro; rewrite (Rmult_comm eps (Rdist x1 x0)) in H3; unfold Rdist in H3, H5; rewrite <- (Rabs_mult (d x0) (x1 - x0)) in H5; rewrite (Rabs_mult 2 (d x0)) in H5; cut (Rabs 2 <> 0). -- intro; fold (Rabs (d x0) > 0) in H1; rewrite (Rinv_mult (Rabs 2) (Rabs (d x0))) in H5; rewrite (Rmult_comm (Rabs (d x0)) (eps * (/ Rabs 2 * / Rabs (d x0)))) in H5; rewrite <- (Rmult_assoc eps (/ Rabs 2) (/ Rabs (d x0))) in H5; rewrite (Rmult_assoc (eps * / Rabs 2) (/ Rabs (d x0)) (Rabs (d x0))) in H5; rewrite (Rinv_l (Rabs (d x0)) (Rlt_dichotomy_converse (Rabs (d x0)) 0 (or_intror (Rabs (d x0) < 0) H1))) in H5; rewrite (let (H1, H2) := Rmult_ne (eps * / Rabs 2) in H1) in H5; cut (Rabs 2 = 2). ++ intro; rewrite H7 in H5; generalize (Rplus_lt_compat (Rabs (d x0 * (x1 - x0))) (eps * / 2) (Rabs (x1 - x0) * eps) (eps * / 2) H5 H3); intro; rewrite eps2 in H10; assumption. ++ unfold Rabs; destruct (Rcase_abs 2) as [Hlt|Hge]; auto. cut (0 < 2). ** intro H7; elim (Rlt_asym 0 2 H7 Hlt). ** lra. -- apply Rabs_no_R0. discrR. Qed.
imports: Rbase Rfunctions Rlimit Lra Lia