proposition: Theorem deriv_maximum : forall f (a b c:R) (pr:derivable_pt f c), a < c -> c < b -> (forall x:R, a < x -> x < b -> f x <= f c) -> derive_pt f c pr = 0.
proof: Proof. intros; case (Rtotal_order 0 (derive_pt f c pr)); intro. { assert (H3 := derivable_derive f c pr). elim H3; intros l H4; rewrite H4 in H2. assert (H5 := derive_pt_eq_1 f c l pr H4). cut (0 < l / 2); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H5 (l / 2) H6); intros delta H7. cut (0 < (b - c) / 2). 1:intro; cut (Rmin (delta / 2) ((b - c) / 2) <> 0). 1:intro; cut (Rabs (Rmin (delta / 2) ((b - c) / 2)) < delta). - intro. assert (H11 := H7 (Rmin (delta / 2) ((b - c) / 2)) H9 H10). cut (0 < Rmin (delta / 2) ((b - c) / 2)). 1:intro; cut (a < c + Rmin (delta / 2) ((b - c) / 2)). 1:intro; cut (c + Rmin (delta / 2) ((b - c) / 2) < b). 1:intro; assert (H15 := H1 (c + Rmin (delta / 2) ((b - c) / 2)) H13 H14). 1:cut ((f (c + Rmin (delta / 2) ((b - c) / 2)) - f c) / Rmin (delta / 2) ((b - c) / 2) <= 0). 1:intro; cut (- l < 0). 1:intro; unfold Rminus in H11. 1:cut ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2) + - l < 0). 1:intro; cut (Rabs ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2) + - l) < l / 2). + unfold Rabs; case (Rcase_abs ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2) + - l)) as [Hlt|Hge]. * replace (- ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2) + - l)) with (l + - ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2))). -- intro; generalize (Rplus_lt_compat_l (- l) (l + - ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2))) (l / 2) H19); repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; replace (- l + l / 2) with (- (l / 2)). ++ intro; generalize (Ropp_lt_gt_contravar (- ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2))) (- (l / 2)) H20); repeat rewrite Ropp_involutive; intro; generalize (Rlt_trans 0 (l / 2) ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2)) H6 H21); intro; elim (Rlt_irrefl 0 (Rlt_le_trans 0 ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2)) 0 H22 H16)). ++ pattern l at 2; rewrite <-Rplus_half_diag. ring. -- ring. * intro. assert (H20 := Rge_le ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2) + - l) 0 Hge). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H20 H18)). + assumption. + rewrite <- Ropp_0; replace ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / Rmin (delta / 2) ((b + - c) / 2) + - l) with (- (l + - ((f (c + Rmin (delta / 2) ((b + - c) / 2)) - f c) / Rmin (delta / 2) ((b + - c) / 2)))). * apply Ropp_gt_lt_contravar; change (0 < l + - ((f (c + Rmin (delta / 2) ((b + - c) / 2)) - f c) / Rmin (delta / 2) ((b + - c) / 2))); apply Rplus_lt_le_0_compat; [ assumption | rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption ]. * unfold Rminus; ring. + rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption. + replace ((f (c + Rmin (delta / 2) ((b - c) / 2)) - f c) / Rmin (delta / 2) ((b - c) / 2)) with (- ((f c - f (c + Rmin (delta / 2) ((b - c) / 2))) / Rmin (delta / 2) ((b - c) / 2))). * rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; [ generalize (Rplus_le_compat_r (- f (c + Rmin (delta * / 2) ((b - c) * / 2))) (f (c + Rmin (delta * / 2) ((b - c) * / 2))) ( f c) H15); rewrite Rplus_opp_r; intro; assumption | left; apply Rinv_0_lt_compat; assumption ]. * unfold Rdiv. rewrite <- Ropp_mult_distr_l_reverse. repeat rewrite <- (Rmult_comm (/ Rmin (delta * / 2) ((b - c) * / 2))). apply Rmult_eq_reg_l with (Rmin (delta * / 2) ((b - c) * / 2)). -- repeat rewrite <- Rmult_assoc. rewrite Rinv_r. ++ repeat rewrite Rmult_1_l. ring. ++ red; intro. unfold Rdiv in H12; rewrite H16 in H12; elim (Rlt_irrefl 0 H12). -- red; intro. unfold Rdiv in H12; rewrite H16 in H12; elim (Rlt_irrefl 0 H12). + assert (H14 := Rmin_r (delta / 2) ((b - c) / 2)). assert (H15 := Rplus_le_compat_l c (Rmin (delta / 2) ((b - c) / 2)) ((b - c) / 2) H14). apply Rle_lt_trans with (c + (b - c) / 2). * assumption. * apply Rmult_lt_reg_l with 2. -- prove_sup0. -- replace (2 * (c + (b - c) / 2)) with (c + b). ++ replace (2 * b) with (b + b). ** apply Rplus_lt_compat_r; assumption. ** ring. ++ unfold Rdiv; rewrite Rmult_plus_distr_l. repeat rewrite (Rmult_comm 2). rewrite Rmult_assoc; rewrite Rinv_l. ** rewrite Rmult_1_r. ring. ** discrR. + apply Rlt_trans with c. * assumption. * pattern c at 1; rewrite <- (Rplus_0_r c); apply Rplus_lt_compat_l; assumption. + cut (0 < delta / 2). * intro; apply (Rmin_stable_in_posreal (mkposreal (delta / 2) H12) (mkposreal ((b - c) / 2) H8)). * unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. - unfold Rabs; case (Rcase_abs (Rmin (delta / 2) ((b - c) / 2))) as [Hlt|Hge]. + cut (0 < delta / 2). * intro. generalize (Rmin_stable_in_posreal (mkposreal (delta / 2) H10) (mkposreal ((b - c) / 2) H8)); simpl; intro; elim (Rlt_irrefl 0 (Rlt_trans 0 (Rmin (delta / 2) ((b - c) / 2)) 0 H11 Hlt)). * unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. + apply Rle_lt_trans with (delta / 2). * apply Rmin_l. * unfold Rdiv; apply Rmult_lt_reg_l with 2. -- prove_sup0. -- rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r. ++ rewrite Rmult_1_l. replace (2 * delta) with (delta + delta). ** pattern delta at 2; rewrite <- (Rplus_0_r delta); apply Rplus_lt_compat_l. rewrite Rplus_0_r; apply (cond_pos delta). ** apply Rplus_diag. ++ discrR. - cut (0 < delta / 2). + intro; generalize (Rmin_stable_in_posreal (mkposreal (delta / 2) H9) (mkposreal ((b - c) / 2) H8)); simpl; intro; red; intro; rewrite H11 in H10; elim (Rlt_irrefl 0 H10). + unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. - unfold Rdiv; apply Rmult_lt_0_compat. + generalize (Rplus_lt_compat_r (- c) c b H0); rewrite Rplus_opp_r; intro; assumption. + apply Rinv_0_lt_compat; prove_sup0. } elim H2; intro. { symmetry ; assumption. } generalize (derivable_derive f c pr); intro; elim H4; intros l H5. rewrite H5 in H3; generalize (derive_pt_eq_1 f c l pr H5); intro; cut (0 < - (l / 2)). - intro; elim (H6 (- (l / 2)) H7); intros delta H9. cut (0 < (c - a) / 2). 1:intro; cut (Rmax (- (delta / 2)) ((a - c) / 2) < 0). 1:intro; cut (Rmax (- (delta / 2)) ((a - c) / 2) <> 0). 1:intro; cut (Rabs (Rmax (- (delta / 2)) ((a - c) / 2)) < delta). 1:intro; generalize (H9 (Rmax (- (delta / 2)) ((a - c) / 2)) H11 H12); intro; cut (a < c + Rmax (- (delta / 2)) ((a - c) / 2)). 1:cut (c + Rmax (- (delta / 2)) ((a - c) / 2) < b). 1:intros; generalize (H1 (c + Rmax (- (delta / 2)) ((a - c) / 2)) H15 H14); intro; cut (0 <= (f (c + Rmax (- (delta / 2)) ((a - c) / 2)) - f c) / Rmax (- (delta / 2)) ((a - c) / 2)). 1:intro; cut (0 < - l). 1:intro; unfold Rminus in H13; cut (0 < (f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) / Rmax (- (delta / 2)) ((a + - c) / 2) + - l). 1:intro; cut (Rabs ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) / Rmax (- (delta / 2)) ((a + - c) / 2) + - l) < - (l / 2)). + unfold Rabs; case (Rcase_abs ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) / Rmax (- (delta / 2)) ((a + - c) / 2) + - l)) as [Hlt|Hge]. * elim (Rlt_irrefl 0 (Rlt_trans 0 ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) / Rmax (- (delta / 2)) ((a + - c) / 2) + - l) 0 H19 Hlt)). * intros; generalize (Rplus_lt_compat_r l ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) / Rmax (- (delta / 2)) ((a + - c) / 2) + - l) ( - (l / 2)) H20); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; replace (- (l / 2) + l) with (l / 2). -- cut (l / 2 < 0). ++ intros; generalize (Rlt_trans ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) / Rmax (- (delta / 2)) ((a + - c) / 2)) (l / 2) 0 H22 H21); intro; elim (Rlt_irrefl 0 (Rle_lt_trans 0 ((f (c + Rmax (- (delta / 2)) ((a - c) / 2)) - f c) / Rmax (- (delta / 2)) ((a - c) / 2)) 0 H17 H23)). ++ rewrite <- (Ropp_involutive (l / 2)); rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption. -- pattern l at 3; rewrite <-Rplus_half_diag. ring. + assumption. + apply Rplus_le_lt_0_compat; assumption. + rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption. + unfold Rdiv; replace ((f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c) * / Rmax (- (delta * / 2)) ((a - c) * / 2)) with (- (f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c) * / - Rmax (- (delta * / 2)) ((a - c) * / 2)). * apply Rmult_le_pos. -- generalize (Rplus_le_compat_l (- f (c + Rmax (- (delta * / 2)) ((a - c) * / 2))) (f (c + Rmax (- (delta * / 2)) ((a - c) * / 2))) ( f c) H16); rewrite Rplus_opp_l; replace (- (f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) - f c)) with (- f (c + Rmax (- (delta * / 2)) ((a - c) * / 2)) + f c). ++ intro; assumption. ++ ring. -- left; apply Rinv_0_lt_compat; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption. * unfold Rdiv. rewrite Rinv_opp. rewrite Rmult_opp_opp. reflexivity. + generalize (Rplus_lt_compat_l c (Rmax (- (delta / 2)) ((a - c) / 2)) 0 H10); rewrite Rplus_0_r; intro; apply Rlt_trans with c; assumption. + generalize (RmaxLess2 (- (delta / 2)) ((a - c) / 2)); intro; generalize (Rplus_le_compat_l c ((a - c) / 2) (Rmax (- (delta / 2)) ((a - c) / 2)) H14); intro; apply Rlt_le_trans with (c + (a - c) / 2). * apply Rmult_lt_reg_l with 2. -- prove_sup0. -- replace (2 * (c + (a - c) / 2)) with (a + c). ++ rewrite <-Rplus_diag. apply Rplus_lt_compat_l; assumption. ++ field; discrR. * assumption. + unfold Rabs; case (Rcase_abs (Rmax (- (delta / 2)) ((a - c) / 2))) as [Hlt|Hge]. * generalize (RmaxLess1 (- (delta / 2)) ((a - c) / 2)); intro; generalize (Ropp_le_ge_contravar (- (delta / 2)) (Rmax (- (delta / 2)) ((a - c) / 2)) H12); rewrite Ropp_involutive; intro; generalize (Rge_le (delta / 2) (- Rmax (- (delta / 2)) ((a - c) / 2)) H13); intro; apply Rle_lt_trans with (delta / 2). -- assumption. -- apply Rmult_lt_reg_l with 2. ++ prove_sup0. ++ unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r. ** rewrite Rmult_1_l; rewrite <-Rplus_diag. pattern delta at 2; rewrite <- (Rplus_0_r delta); apply Rplus_lt_compat_l; rewrite Rplus_0_r; apply (cond_pos delta). ** discrR. * cut (- (delta / 2) < 0). -- cut ((a - c) / 2 < 0). ++ intros; generalize (Rmax_stable_in_negreal (mknegreal (- (delta / 2)) H13) (mknegreal ((a - c) / 2) H12)); simpl; intro; generalize (Rge_le (Rmax (- (delta / 2)) ((a - c) / 2)) 0 Hge); intro; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (Rmax (- (delta / 2)) ((a - c) / 2)) 0 H15 H14)). ++ rewrite <- Ropp_0; rewrite <- (Ropp_involutive ((a - c) / 2)); apply Ropp_lt_gt_contravar; replace (- ((a - c) / 2)) with ((c - a) / 2). ** assumption. ** unfold Rdiv. rewrite <- Ropp_mult_distr_l_reverse. rewrite (Ropp_minus_distr a c). reflexivity. -- rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ]. + red; intro; rewrite H11 in H10; elim (Rlt_irrefl 0 H10). + cut ((a - c) / 2 < 0). * intro; cut (- (delta / 2) < 0). -- intro; apply (Rmax_stable_in_negreal (mknegreal (- (delta / 2)) H11) (mknegreal ((a - c) / 2) H10)). -- rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ]. * rewrite <- Ropp_0; rewrite <- (Ropp_involutive ((a - c) / 2)); apply Ropp_lt_gt_contravar; replace (- ((a - c) / 2)) with ((c - a) / 2). -- assumption. -- unfold Rdiv. rewrite <- Ropp_mult_distr_l_reverse. rewrite (Ropp_minus_distr a c). reflexivity. + unfold Rdiv; apply Rmult_lt_0_compat; [ generalize (Rplus_lt_compat_r (- a) a c H); rewrite Rplus_opp_r; intro; assumption | assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ] ]. - replace (- (l / 2)) with (- l / 2). + unfold Rdiv; apply Rmult_lt_0_compat. * rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption. * assert (Hyp : 0 < 2); [ prove_sup0 | apply (Rinv_0_lt_compat 2 Hyp) ]. + unfold Rdiv; apply Ropp_mult_distr_l_reverse. Qed.
imports: Rbase Rfunctions Rlimit Rderiv