proposition: Lemma Taylor_lemma11 : forall n Hf Hf' H, {c : IR | I c | forall Hc, AbsIR (g' n Hf Hf' H c Hc) [<=] e[*]AbsIR ([1][/] (b[-]a) [//]H)}.
proof: Proof. intros. cut (Dom (g n Hf H) (Min a b)). intro H0. cut (Dom (g n Hf H) (Max a b)). intro H1. cut (Dom (g n Hf H) a). intro H2. cut (Dom (g n Hf H) b). intro H3. unfold I, Hab in |- *; apply Rolle with (g n Hf H) H0 H1. apply Taylor_lemma10; auto. elim (ap_imp_less _ _ _ Hap); intro. apply eq_transitive_unfolded with ZeroR. eapply eq_transitive_unfolded. 2: apply Taylor_lemma4 with (Ha' := H2). apply pfwdef; apply leEq_imp_Min_is_lft; apply less_leEq; auto. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. 2: apply Taylor_lemma5 with (Hb' := H3). apply pfwdef; apply leEq_imp_Max_is_rht; apply less_leEq; auto. apply eq_transitive_unfolded with ZeroR. eapply eq_transitive_unfolded. 2: apply Taylor_lemma5 with (Hb' := H3). apply pfwdef; eapply eq_transitive_unfolded. apply Min_comm. apply leEq_imp_Min_is_lft; apply less_leEq; auto. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. 2: apply Taylor_lemma4 with (Ha' := H2). apply pfwdef; eapply eq_transitive_unfolded. apply Max_comm. apply leEq_imp_Max_is_rht; apply less_leEq; auto. astepl ([0][*]AbsIR ([1][/] _[//]H)). apply mult_resp_less. assumption. apply AbsIR_pos. apply div_resp_ap_zero_rev. apply one_ap_zero. split; split; split; simpl in |- *; auto. 3: split; split. 2: split; split; auto; apply TL_compact_b. apply FSumx_pred'; intros. 2: apply TL_b_i'. red in |- *; intros. try rename X into H6. exact (Taylor_lemma3' _ _ _ _ H3 _ _ _ _ H4 H6). split; split; split; simpl in |- *; auto. 3: split; split. 2: split; split; auto; apply TL_compact_a. apply FSumx_pred'; intros. 2: apply TL_a_i'. red in |- *; intros. try rename X into H5. exact (Taylor_lemma3' _ _ _ _ H2 _ _ _ _ H3 H5). split; split; split; simpl in |- *; auto. 3: split; split. 2: split; split; auto; apply compact_inc_rht. apply FSumx_pred'; intros. 2: apply TL_x_i'. red in |- *; intros. try rename X into H4. exact (Taylor_lemma3' _ _ _ _ H1 _ _ _ _ H2 H4). unfold I in |- *; apply compact_inc_rht. split; split; split; simpl in |- *; auto. 3: split; split. 2: split; split; auto; apply compact_inc_lft. apply FSumx_pred'; intros. 2: apply TL_x_i'. red in |- *; intros. try rename X into H3. exact (Taylor_lemma3' _ _ _ _ H0 _ _ _ _ H1 H3). unfold I in |- *; apply compact_inc_lft. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)