proposition: Lemma is_RInt_gen_Derive {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb} (f : R -> R) (la lb : R) : filter_prod Fa Fb (fun ab => forall x : R, Rmin (fst ab) (snd ab) <= x <= Rmax (fst ab) (snd ab) -> ex_derive f x) -> filter_prod Fa Fb (fun ab => forall x : R, Rmin (fst ab) (snd ab) <= x <= Rmax (fst ab) (snd ab) -> continuous (Derive f) x) -> filterlim f Fa (locally la) -> filterlim f Fb (locally lb) -> is_RInt_gen (Derive f) Fa Fb (lb - la).
proof: Proof. intros Df Cf Lfa Lfb P HP. assert (HP': filter_prod Fa Fb (fun ab => P (f (snd ab) - f (fst ab)))). unfold Rminus. eapply filterlim_comp_2. eapply filterlim_comp, Lfb. by apply filterlim_snd. eapply filterlim_comp, @filterlim_opp. eapply filterlim_comp, Lfa. by apply filterlim_fst. exact: (filterlim_plus lb (- la)). exact HP. apply: filter_imp (filter_and _ _ (filter_and _ _ Df Cf) HP'). move => [a b] /= {Df Cf HP HP'} [[Df Cf] HP]. eexists. apply: conj HP. apply: is_RInt_derive => x Hx. now apply Derive_correct, Df. exact: Cf. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis