proposition: Lemma IAF_var : forall (f g:R -> R) (a b:R) (pr1:derivable f) (pr2:derivable g), a <= b -> (forall c:R, a <= c <= b -> derive_pt g c (pr2 c) <= derive_pt f c (pr1 c)) -> g b - g a <= f b - f a.
proof: Proof. intros. assert (X:derivable (g - f)) by (apply derivable_minus; assumption). assert (forall c:R, a <= c <= b -> derive_pt (g - f) c (X c) <= 0). { intros. assert (derive_pt (g - f) c (X c) = derive_pt (g - f) c (derivable_pt_minus _ _ _ (pr2 c) (pr1 c))) by apply pr_nu. rewrite H2. rewrite derive_pt_minus. apply Rplus_le_reg_l with (derive_pt f c (pr1 c)). rewrite Rplus_0_r. replace (derive_pt f c (pr1 c) + (derive_pt g c (pr2 c) - derive_pt f c (pr1 c))) with (derive_pt g c (pr2 c)); [ idtac | ring ]. apply H0; assumption. } assert (H2 := IAF (g - f)%F a b 0 X H H1). unfold minus_fct in H2. lra. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra