proposition: Lemma L_diffble : forall (n : nat) (f : C_inf_ab c d Hcd), Diffble_I_n Hab n (L_func f).
proof: Proof. intro n. induction n. intro f0. unfold L_func. simpl. unfold included. intros. assert (Conj (fun _ : IR => True) (Conj (Conj (fun _ : IR => True) (fun _ : IR => True)) (Conj (Conj (fun _ : IR => True) (fun _ : IR => True)) (extend (Conj (fun _ : IR => True) (fun _ : IR => True)) (fun (x0 : IR) (_ : Conj (fun _ : IR => True) (fun _ : IR => True) x0) => b[-]a[#]Zero)))) x). unfold extend. red. split. auto. red. split. red. auto. red. split. red. auto. split. red. auto. intro. apply ab_diff. exists X. destruct f0. replace (f_crr c d Hcd (Build_C_inf_ab c d Hcd f_crr0 f_pdf0)) with f_crr0 by auto. destruct f_crr0. simpl. assert (included (Compact (less_leEq _ _ _ Hcd)) pfdom). assert (Diffble_I_n Hcd 0 (Build_PartFunct IR pfdom dom_wd pfpfun pfstrx)). apply f_pdf0. simpl in X0. exact X0. unfold included in X0. apply X0. red. split. red in H. rewrite <- cm_rht_unit_unfolded at 1. apply plus_resp_leEq_lft. rewrite <- (cring_mult_zero_op IR Zero). apply mult_resp_leEq_both. apply leEq_reflexive. apply leEq_reflexive. apply shift_leEq_lft. algebra. apply shift_leEq_div. apply shift_zero_less_minus. exact Hab. rewrite cring_mult_zero_op. apply shift_leEq_lft. inversion H. exact H0. apply shift_plus_leEq'. rewrite <- (mult_one IR (d[-]c)) at 2. apply mult_resp_leEq_both. apply shift_leEq_lft. algebra. apply shift_leEq_div. apply shift_zero_less_minus. exact Hab. rewrite cring_mult_zero_op. red in H. inversion H. apply shift_leEq_lft. exact H0. apply leEq_reflexive. apply shift_div_leEq. apply shift_zero_less_minus. exact Hab. rewrite mult_commutes. rewrite mult_one. apply minus_resp_leEq_both. red in H. inversion H. exact H1. apply leEq_reflexive. intro f0. simpl. assert (Derivative_I Hab L_inner ( ([-C-] Zero) {+} ( ([-C-] d {-} [-C-] c) {*} ( Fdiv ((([-C-] One) {*} ([-C-] b {-} [-C-] a)) {-} ((Fid IR {-} [-C-] a) {*} ([-C-] Zero))) (([-C-] b {-} [-C-] a) {*} ([-C-] b {-} [-C-] a)) ) {+} ([-C-] Zero) {*} ( Fdiv (Fid IR {-} [-C-] a) ([-C-] b {-} [-C-] a) ) ) )). unfold L_inner. apply Derivative_I_plus. apply Derivative_I_const. apply Derivative_I_mult. apply Derivative_I_wdr with ([-C-]Zero{-}[-C-]Zero). FEQ. apply Derivative_I_minus. apply Derivative_I_const. apply Derivative_I_const. apply Derivative_I_div. apply Derivative_I_wdr with ([-C-]One{-}[-C-]Zero). FEQ. apply Derivative_I_minus. apply Derivative_I_id. apply Derivative_I_const. apply Derivative_I_wdr with ([-C-]Zero{-}[-C-]Zero). FEQ. apply Derivative_I_minus. apply Derivative_I_const. apply Derivative_I_const. red. split. apply included_FMinus. unfold included; simpl; auto. unfold included; simpl; auto. exists (AbsIR (b[-]a)). apply AbsIR_pos. apply ab_diff. intros. simpl. apply leEq_reflexive. assert (Diffble_I Hcd (f_crr c d Hcd f0)). destruct f0; simpl. apply Diffble_I_n_imp_diffble with 42. omega. apply f_pdf0. destruct X0. assert (forall n, Diffble_I_n Hcd n (PartInt x)). intro n0. replace n0 with (pred (S n0)) by omega. apply Diffble_I_imp_le with (f_crr c d Hcd f0). omega. destruct f0. replace (f_crr c d Hcd (Build_C_inf_ab c d Hcd f_crr0 f_pdf0)) with f_crr0 by auto. apply f_pdf0. exact d0. assert (Derivative_I Hab (L_func f0) ((L_func (Build_C_inf_ab c d Hcd (PartInt x) X0)) {*} (([-C-]Zero{+} (([-C-]d{-}[-C-]c){*} (([-C-]One{*}([-C-]b{-}[-C-]a){-}(FId{-}[-C-]a){*}[-C-]Zero){/} ([-C-]b{-}[-C-]a){*}([-C-]b{-}[-C-]a)){+} [-C-]Zero{*}((FId{-}[-C-]a){/}([-C-]b{-}[-C-]a)))))) ). unfold L_func. apply (Derivative_I_comp _ _ _ _ _ _ _ c d Hcd). exact X. simpl. exact d0. unfold maps_into_compacts. split. destruct f0. simpl. apply Diffble_I_n_imp_inc with 42. apply f_pdf0. intros. red. split. unfold L_inner. simpl. rewrite <- cm_rht_unit_unfolded at 1. apply plus_resp_leEq_lft. rewrite <- (cring_mult_zero_op IR Zero). apply mult_resp_leEq_both. apply leEq_reflexive. apply leEq_reflexive. apply shift_leEq_lft. algebra. apply shift_leEq_div. apply shift_zero_less_minus. exact Hab. rewrite cring_mult_zero_op. apply shift_leEq_lft. inversion H. exact H0. unfold L_inner. simpl. apply shift_plus_leEq'. rewrite <- (mult_one IR (d[-]c)) at 2. apply mult_resp_leEq_both. apply shift_leEq_lft. algebra. apply shift_leEq_div. apply shift_zero_less_minus. exact Hab. rewrite cring_mult_zero_op. inversion H. apply shift_leEq_lft. exact H0. apply leEq_reflexive. apply shift_div_leEq. apply shift_zero_less_minus. exact Hab. rewrite mult_commutes. rewrite mult_one. apply minus_resp_leEq_both. inversion H. exact H1. apply leEq_reflexive. assert (Diffble_I Hab (L_func f0)). apply (deriv_imp_Diffble_I _ _ _ _ _ X1). exists X2. destruct X2. simpl. apply Diffble_I_n_wd with (L_func (Build_C_inf_ab c d Hcd (PartInt x) X0){*} ([-C-]Zero{+}(([-C-]d{-}[-C-]c){*} (([-C-]One{*}([-C-]b{-}[-C-]a){-}(FId{-}[-C-]a){*}[-C-]Zero){/} ([-C-]b{-}[-C-]a){*}([-C-]b{-}[-C-]a)){+} [-C-]Zero{*}((FId{-}[-C-]a){/}([-C-]b{-}[-C-]a))))). apply Derivative_I_unique with (L_func f0). exact X1. exact d1. apply Diffble_I_n_mult. apply IHn. apply Diffble_I_n_plus. apply Diffble_I_n_const. apply Diffble_I_n_plus. apply Diffble_I_n_mult. apply Diffble_I_n_minus. apply Diffble_I_n_const. apply Diffble_I_n_const. apply Diffble_I_n_div. apply Diffble_I_n_minus. apply Diffble_I_n_mult. apply Diffble_I_n_const. apply Diffble_I_n_minus. apply Diffble_I_n_const. apply Diffble_I_n_const. apply Diffble_I_n_wd with ([-C-] Zero). FEQ. apply Diffble_I_n_const. apply Diffble_I_n_mult. apply Diffble_I_n_minus. apply Diffble_I_n_const. apply Diffble_I_n_const. apply Diffble_I_n_minus. apply Diffble_I_n_const. apply Diffble_I_n_const. unfold bnd_away_zero. split. apply included_FMult. apply included_FMinus. unfold included; simpl; auto. unfold included; simpl; auto. apply included_FMinus. unfold included; simpl; auto. unfold included; simpl; auto. exists ((b[-]a)[*](b[-]a)). apply mult_resp_pos. apply shift_zero_less_minus. exact Hab. apply shift_zero_less_minus. exact Hab. intros. rewrite AbsIR_resp_mult. apply mult_resp_leEq_both. apply shift_zero_leEq_minus. algebra. apply shift_zero_leEq_minus. algebra. apply eq_imp_leEq. symmetry. apply AbsIR_eq_x. apply shift_zero_leEq_minus. algebra. apply eq_imp_leEq. symmetry. apply AbsIR_eq_x. algebra. apply Diffble_I_n_wd with ([-C-] Zero). apply eq_imp_Feq. unfold included; simpl; auto. apply included_FMult. unfold included; simpl; auto. apply included_FDiv. apply included_FMinus. unfold included; simpl; auto. unfold included; simpl; auto. apply included_FMinus. unfold included; simpl; auto. unfold included; simpl; auto. intros. simpl. apply pos_ap_zero. apply shift_zero_less_minus. exact Hab. intros. simpl. rewrite mult_commutes. rewrite cring_mult_zero. reflexivity. apply Diffble_I_n_const. Qed.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass Structures