(**
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Copyright (C) 2011-2015 Sylvie Boldo
#<br />#
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Copyright (C) 2011-2015 Catherine Lelay
#<br />#
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Copyright (C) 2011-2015 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

Require Import Reals mathcomp.ssreflect.ssreflect.
Require Import Rbar Hierarchy RInt Lim_seq Continuity Derive.
Require Import Rcomplements RInt_analysis.

(** This file describes improper integrals, such as integrals with an
infinity endpoint or integrals of a function with a singularity. A few
properties are given: Chasles, operations, composition, derivation.*)

Open Scope R_scope.

(** * Improper Riemann integral *)

Section is_RInt_gen.

Context {V : NormedModule R_AbsRing}.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Definition is_RInt_gen (f : R -> V) (Fa Fb : (R -> Prop) -> Prop) (l : V) :=
  filterlimi (fun ab => is_RInt f (fst ab) (snd ab)) (filter_prod Fa Fb) (locally l).
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Definition ex_RInt_gen (f : R -> V) (Fa Fb : (R -> Prop) -> Prop) :=
  exists l : V, is_RInt_gen f Fa Fb l.

Definition is_RInt_gen_at_point f a b l :
  is_RInt_gen f (at_point a) (at_point b) l
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
    <-> is_RInt f a b l.
Proof.
(* Goal: and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) (P (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) *)
split.
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
- intros H P HP.
(* Goal: @filtermap (@SF_seq.SF_seq R) (ModuleSpace.sort R_Ring (NormedModule.ModuleSpace R_AbsRing V)) (fun ptd : @SF_seq.SF_seq R => @scal R_Ring (NormedModule.ModuleSpace R_AbsRing V) (sign (Rminus b a)) (@SF_seq.Riemann_sum (NormedModule.ModuleSpace R_AbsRing V) f ptd)) (SF_seq.Riemann_fine a b) P *)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  apply locally_locally in HP.
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V (fun y : R => @opp (NormedModule.AbelianGroup R_AbsRing V) (f y)) (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fb) P *)
  specialize (H _ HP).
(* Goal: @filtermap (@SF_seq.SF_seq R) (ModuleSpace.sort R_Ring (NormedModule.ModuleSpace R_AbsRing V)) (fun ptd : @SF_seq.SF_seq R => @scal R_Ring (NormedModule.ModuleSpace R_AbsRing V) (sign (Rminus b a)) (@SF_seq.Riemann_sum (NormedModule.ModuleSpace R_AbsRing V) f ptd)) (SF_seq.Riemann_fine a b) P *)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  destruct H as [Q R Qa Rb H].
(* Goal: @filtermap (@SF_seq.SF_seq R) (ModuleSpace.sort R_Ring (NormedModule.ModuleSpace R_AbsRing V)) (fun ptd : @SF_seq.SF_seq R => @scal R_Ring (NormedModule.ModuleSpace R_AbsRing V) (sign (Rminus b a)) (@SF_seq.Riemann_sum (NormedModule.ModuleSpace R_AbsRing V) f ptd)) (SF_seq.Riemann_fine a b) P *)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  destruct (H a b Qa Rb) as [y [Hy1 Hy2]].
(* Goal: @filtermap (@SF_seq.SF_seq R) (ModuleSpace.sort R_Ring (NormedModule.ModuleSpace R_AbsRing V)) (fun ptd : @SF_seq.SF_seq R => @scal R_Ring (NormedModule.ModuleSpace R_AbsRing V) (sign (Rminus b a)) (@SF_seq.Riemann_sum (NormedModule.ModuleSpace R_AbsRing V) f ptd)) (SF_seq.Riemann_fine a b) P *)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  now apply Hy1.
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
- intros Hl P HP.
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) P *)
  exists (fun x => x = a) (fun x => x = b) ; try easy.
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  intros x y -> ->.
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst R R (@pair (UniformSpace.sort R_UniformSpace) (UniformSpace.sort R_UniformSpace) a b)) (@snd R R (@pair (UniformSpace.sort R_UniformSpace) (UniformSpace.sort R_UniformSpace) a b)) y) (P y)) *)
  exists l.
(* Goal: and (@is_RInt V f (@fst R R (@pair (UniformSpace.sort R_UniformSpace) (UniformSpace.sort R_UniformSpace) a b)) (@snd R R (@pair (UniformSpace.sort R_UniformSpace) (UniformSpace.sort R_UniformSpace) a b)) l) (P l) *)
  apply (conj Hl).
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
  exact: locally_singleton.
Qed.

(** * Basic properties of integrals *)

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_ext {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) (l : V) :
  filter_prod Fa Fb (fun ab => forall x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
                               -> f x = g x) ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fa Fb l -> is_RInt_gen g Fa Fb l.
Proof.
intros Heq.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: filterlimi_ext_loc.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: filter_imp Heq.
intros [a b] Heq y.
(* Goal: and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) (P (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) *)
split.
now apply is_RInt_ext.
apply is_RInt_ext.
intros x Hx.
now apply sym_eq, Heq.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma ex_RInt_gen_ext {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) :
  filter_prod Fa Fb (fun ab => forall x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
                               -> f x = g x) ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  ex_RInt_gen f Fa Fb -> ex_RInt_gen g Fa Fb.
Proof.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => Heq.
(* Goal: forall _ : ex_RInt_gen f Fa Fb, ex_RInt_gen g Fa Fb *)
case => I HI.
(* Goal: ex_RInt_gen g Fa Fb *)
exists I.
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
exact: (is_RInt_gen_ext f g).
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma ex_RInt_gen_ext_eq {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  (forall x, f x = g x) -> ex_RInt_gen f Fa Fb -> ex_RInt_gen g Fa Fb.
Proof.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => Heq.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: ex_RInt_gen_ext.
(* Goal: forall _ : @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b I, @ex_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) *)
exact: filter_forall => bds x _.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_point (f : R -> V) (a : R) :
  is_RInt_gen f (at_point a) (at_point a) zero.
Proof.
(* Goal: @is_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) (@RInt V f a b) *)
  apply is_RInt_gen_at_point.
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
  exact: is_RInt_point.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_swap {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f : R -> V) (l : V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fb Fa l -> is_RInt_gen f Fa Fb (opp l).
Proof.
(* Goal: forall _ : is_RInt_gen f Fb Fa l, is_RInt_gen f Fa Fb (@opp (NormedModule.AbelianGroup R_AbsRing V) l) *)
intros Hf P HP.
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fb) P *)
specialize (Hf (fun y => P (opp y))).
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fb) P *)
destruct Hf as [Q R HQ HR H].
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
  exact: filterlim_opp.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: Filter_prod HR HQ _ => a b Ha Hb.
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a b)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a b)) y) (P y)) *)
specialize (H b a Hb Ha).
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a b)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a b)) y) (P y)) *)
destruct H as [y [Hy1 Hy2]].
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V (fun y0 : R => @opp (NormedModule.AbelianGroup R_AbsRing V) (f y0)) a b y) (P y)) *)
exists (opp y).
(* Goal: and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) (P (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) *)
split.
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
exact: is_RInt_swap.
(* Goal: P (@opp (NormedModule.AbelianGroup R_AbsRing V) y) *)
exact Hy2.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_Chasles {Fa Fc : (R -> Prop) -> Prop}
  {FFa : Filter Fa} {FFc : Filter Fc}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  (f : R -> V) (b : R) (l1 l2 : V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fa (at_point b) l1 -> is_RInt_gen f (at_point b) Fc l2
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  -> is_RInt_gen f Fa Fc (plus l1 l2).
Proof.
(* Goal: forall (_ : is_RInt_gen f Fa (@at_point R_UniformSpace b) l1) (_ : is_RInt_gen f (@at_point R_UniformSpace b) Fc l2), is_RInt_gen f Fa Fc (@plus (NormedModule.AbelianGroup R_AbsRing V) l1 l2) *)
intros Hab Hbc P HP.
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fc) P *)
specialize (filterlim_plus _ _ P HP).
(* Goal: forall _ : @filtermap (prod (NormedModule.sort R_AbsRing V) (NormedModule.sort R_AbsRing V)) (AbelianGroup.sort (NormedModule.AbelianGroup R_AbsRing V)) (fun z : prod (NormedModule.sort R_AbsRing V) (NormedModule.sort R_AbsRing V) => @plus (NormedModule.AbelianGroup R_AbsRing V) (@fst (NormedModule.sort R_AbsRing V) (NormedModule.sort R_AbsRing V) z) (@snd (NormedModule.sort R_AbsRing V) (NormedModule.sort R_AbsRing V) z)) (@filter_prod (UniformSpace.sort (NormedModule.UniformSpace R_AbsRing V)) (UniformSpace.sort (NormedModule.UniformSpace R_AbsRing V)) (@locally (NormedModule.UniformSpace R_AbsRing V) l1) (@locally (NormedModule.UniformSpace R_AbsRing V) l2)) P, @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fc) P *)
intros [Q R HQ HR H].
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fc) P *)
specialize (Hab Q HQ).
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fc) P *)
specialize (Hbc R HR).
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fc) P *)
destruct Hab as [Qa Ra HQa HRa Hab].
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V f (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fc) P *)
destruct Hbc as [Qc Rc HQc HRc Hbc].
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: Filter_prod HQa HRc _.
(* Goal: forall (x y : Rdefinitions.R) (_ : Qa x) (_ : Rc y), @ex (NormedModule.sort R_AbsRing V) (fun y0 : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R x y)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R x y)) y0) (P y0)) *)
intros a c Ha Hc.
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) y) (P y)) *)
specialize (Hab _ _ Ha HRa).
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) y) (P y)) *)
specialize (Hbc _ _ HQc Hc).
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) y) (P y)) *)
destruct Hab as [ya [Hya1 Hya2]].
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) y) (P y)) *)
destruct Hbc as [yc [Hyc1 Hyc2]].
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) y) (P y)) *)
exists (plus ya yc).
(* Goal: and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) (P (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) *)
split.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: is_RInt_Chasles Hya1 Hyc1.
(* Goal: P (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc) *)
now apply H.
Qed.

(** * Composition *)

(*
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_comp_opp {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f : R -> V) (l : V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f (filtermap opp Fa) (filtermap opp Fb) l ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen (fun y => opp (f (- y))) Fa Fb l.
Proof.
intros H.
apply: filterlimi_ext.
unfold is_RInt_gen.
apply: filterlimi_comp_2.
apply filterlim_fst.
apply filterlim_snd.
SearchAbout fst filter_prod.

  case => If [Hf Hl].
(* Goal: and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) (P (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) *)
  exists (fun x => If (opp x)) ; split.
  case: Hf => P Q ;
  unfold filtermap => Pa Qb H.
  eexists ; try eassumption.
  move => /= a b Ha Hb.
  by apply is_RInt_comp_opp, H.
  eapply filterlim_comp, Hl.
  intros P [Q1 Q2 Q1a Q2b H].
  eexists ; try eassumption.
  move => /= a b Ha Hb.
  by apply H.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_comp_lin {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f : R -> V) (u v : R) (l : V) :
  is_RInt_gen f (filtermap (fun a => u * a + v) Fa) (filtermap (fun b => u * b + v) Fb) l
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
    -> is_RInt_gen (fun y => scal u (f (u * y + v))) Fa Fb l.
Proof.
  case => If [Hf Hl].
(* Goal: and (@is_RInt V f (@fst Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@snd Rdefinitions.R Rdefinitions.R (@pair Rdefinitions.R Rdefinitions.R a c)) (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) (P (@plus (NormedModule.AbelianGroup R_AbsRing V) ya yc)) *)
  exists (fun x => If (plus (scal u x) (v,v))) ; split.
  case: Hf => P Q ;
  unfold filtermap => Pa Qb H.
  eexists ; try eassumption.
  move => /= a b Ha Hb.
  by apply is_RInt_comp_lin, H.
  eapply filterlim_comp, Hl.
  intros P [Q1 Q2 Q1a Q2b H].
  eexists ; try eassumption.
  move => /= a b Ha Hb.
  by apply H.
Qed.
*)

(** * Operations *)

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_scal {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f : R -> V) (k : R) (l : V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fa Fb l ->
  is_RInt_gen (fun y => scal k (f y)) Fa Fb (scal k l).
Proof.
(* Goal: forall _ : is_RInt_gen f Fa Fb l, is_RInt_gen (fun y : R => @opp (NormedModule.AbelianGroup R_AbsRing V) (f y)) Fa Fb (@opp (NormedModule.AbelianGroup R_AbsRing V) l) *)
intros H P HP.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move /filterlim_scal_r in HP.
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V (fun y : R => @opp (NormedModule.AbelianGroup R_AbsRing V) (f y)) (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fb) P *)
specialize (H _ HP).
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
unfold filtermapi in H |- *.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: filter_imp H.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => [a b] /= [y [Hy1 Hy2]].
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V (fun y0 : R => @scal R_Ring (NormedModule.ModuleSpace R_AbsRing V) k (f y0)) a b y) (P y)) *)
exists (scal k y).
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: conj Hy2.
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
exact: is_RInt_scal.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_opp {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f : R -> V) (l : V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fa Fb l ->
  is_RInt_gen (fun y => opp (f y)) Fa Fb (opp l).
Proof.
(* Goal: forall _ : is_RInt_gen f Fa Fb l, is_RInt_gen (fun y : R => @opp (NormedModule.AbelianGroup R_AbsRing V) (f y)) Fa Fb (@opp (NormedModule.AbelianGroup R_AbsRing V) l) *)
intros H P HP.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move /filterlim_opp in HP.
(* Goal: @filtermapi (prod R R) (NormedModule.sort R_AbsRing V) (fun ab : prod R R => @is_RInt V (fun y : R => @opp (NormedModule.AbelianGroup R_AbsRing V) (f y)) (@fst R R ab) (@snd R R ab)) (@filter_prod R R Fa Fb) P *)
specialize (H _ HP).
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
unfold filtermapi in H |- *.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: filter_imp H.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => [a b] /= [y [Hy1 Hy2]].
(* Goal: @ex (NormedModule.sort R_AbsRing V) (fun y : NormedModule.sort R_AbsRing V => and (@is_RInt V (fun y0 : R => @opp (NormedModule.AbelianGroup R_AbsRing V) (f y0)) a b y) (P y)) *)
exists (opp y).
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: conj Hy2.
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
exact: is_RInt_opp.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_plus {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) (lf lg : V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fa Fb lf ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen g Fa Fb lg ->
  is_RInt_gen (fun y => plus (f y) (g y)) Fa Fb (plus lf lg).
Proof.
intros Hf Hg P HP.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move /filterlim_plus in HP.
destruct HP as [Q R HQ HR H].
specialize (Hf _ HQ).
specialize (Hg _ HR).
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
unfold filtermapi in Hf, Hg |- *.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: filter_imp (filter_and _ _ Hf Hg).
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => [a b] /= [[If [HIf1 HIf2]] [Ig [HIg1 HIg2]]].
exists (plus If Ig).
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: conj (H _ _ HIf2 HIg2).
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
exact: is_RInt_plus.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_minus {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) (lf lg : V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fa Fb lf ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen g Fa Fb lg ->
  is_RInt_gen (fun y => minus (f y) (g y)) Fa Fb (minus lf lg).
Proof.
(* Goal: forall (_ : is_RInt_gen f Fa Fb lf) (_ : is_RInt_gen g Fa Fb lg), is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
intros Hf Hg.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: is_RInt_gen_plus Hf _.
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
exact: is_RInt_gen_opp.
Qed.

End is_RInt_gen.

Section RInt_gen.

Context {V : CompleteNormedModule R_AbsRing}.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Definition RInt_gen (f : R -> V) (a b : (R -> Prop) -> Prop) :=
  iota (is_RInt_gen f a b).

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_unique {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : ProperFilter' Fa} {FFb : ProperFilter' Fb} (f : R -> V) (l : V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fa Fb l -> RInt_gen f Fa Fb = l.
Proof.
(* Goal: forall _ : @is_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f Fa Fb l, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (RInt_gen f Fa Fb) l *)
apply iota_filterlimi_locally.
(* Goal: @filter_prod R R Fa Fb (fun x : prod R R => forall (y1 y2 : CompleteNormedModule.sort R_AbsRing V) (_ : @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f (@fst R R x) (@snd R R x) y1) (_ : @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f (@fst R R x) (@snd R R x) y2), @eq (CompleteNormedModule.sort R_AbsRing V) y1 y2) *)
apply filter_forall.
(* Goal: forall (x : prod R R) (y1 y2 : CompleteNormedModule.sort R_AbsRing V) (_ : @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f (@fst R R x) (@snd R R x) y1) (_ : @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f (@fst R R x) (@snd R R x) y2), @eq (CompleteNormedModule.sort R_AbsRing V) y1 y2 *)
intros [a b] y1 u2 H1 H2.
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
rewrite -(is_RInt_unique _ _ _ _ H1).
(* Goal: @eq (CompleteNormedModule.sort R_AbsRing V) (@RInt V f (@fst R R (@pair R R a b)) (@snd R R (@pair R R a b))) u2 *)
now apply is_RInt_unique.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma RInt_gen_correct {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : ProperFilter' Fa} {FFb : ProperFilter' Fb} (f : R -> V) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  ex_RInt_gen f Fa Fb -> is_RInt_gen f Fa Fb (RInt_gen f Fa Fb).
Proof.
(* Goal: forall _ : @ex_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f Fa Fb, @is_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f Fa Fb (RInt_gen f Fa Fb) *)
intros [If HIf].
(* Goal: @is_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f Fa Fb (RInt_gen f Fa Fb) *)
erewrite is_RInt_gen_unique ; exact HIf.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma RInt_gen_norm {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f : R -> V) (g : R -> R) (lf : V) (lg : R) :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  filter_prod Fa Fb (fun ab => fst ab <= snd ab) ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  filter_prod Fa Fb (fun ab => forall x, fst ab <= x <= snd ab -> norm (f x) <= g x) ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  is_RInt_gen f Fa Fb lf -> is_RInt_gen g Fa Fb lg ->
  norm lf <= lg.
Proof.
intros Hab Hle Hf Hg.
apply (filterlim_le (F := filter_prod Fa Fb) (fun ab => norm (RInt f (fst ab) (snd ab))) (fun ab => RInt g (fst ab) (snd ab)) (norm lf) lg).
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
- specialize (Hf _ (locally_ball lf (mkposreal _ Rlt_0_1))).
  specialize (Hg _ (locally_ball lg (mkposreal _ Rlt_0_1))).
  unfold filtermapi in Hf, Hg.
  apply: filter_imp (filter_and _ _ (filter_and  _ _ Hf Hg) (filter_and _ _ Hab Hle)) => {Hf Hg Hab Hle}.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
  move => [a b] /= [[[If [Hf1 Hf2]] [Ig [Hg1 Hg2]]] [H H']].
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
  apply: norm_RInt_le H H' _ _.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
  apply: RInt_correct.
  now exists If.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
  apply: RInt_correct.
  now exists Ig.
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
- eapply filterlim_comp, filterlim_norm.
  intros P HP.
  specialize (Hf P HP).
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  unfold filtermapi, filtermap in Hf |- *.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
  apply: filter_imp Hf.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
  move => [a b] /= [y [Hy1 Hy2]].
  now rewrite (is_RInt_unique _ a b y Hy1).
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
- intros P HP.
  specialize (Hg P HP).
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  unfold filtermapi, filtermap in Hg |- *.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
  apply: filter_imp Hg.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
  move => [a b] /= [y [Hy1 Hy2]].
  now rewrite (is_RInt_unique _ a b y Hy1).
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma RInt_gen_ext {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f g : R -> V) :
  filter_prod Fa Fb (fun ab => forall x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
                               -> f x = g x) ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  ex_RInt_gen f Fa Fb -> RInt_gen f Fa Fb = RInt_gen g Fa Fb.
Proof.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => Heq [I HI].
(* Goal: @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (RInt_gen f Fa Fb) (RInt_gen g Fa Fb) *)
rewrite (is_RInt_gen_unique f I HI); symmetry.
(* Goal: @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
apply is_RInt_gen_unique. (* 'apply:' does not work *)
(* Goal: @ex_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) *)
by apply: is_RInt_gen_ext; first exact: Heq.
Qed.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma RInt_gen_ext_eq {Fa Fb : (R -> Prop) -> Prop}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  {FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f g : R -> V):
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  (forall x, f x = g x) ->
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  ex_RInt_gen f Fa Fb -> RInt_gen f Fa Fb = RInt_gen g Fa Fb.
Proof.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => Heq.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: (RInt_gen_ext f g).
(* Goal: forall _ : @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b I, @ex_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) *)
exact: filter_forall => bnds x _.
Qed.

End RInt_gen.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma is_RInt_gen_Derive {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb}
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  (f : R -> R) (la lb : R) :
  filter_prod Fa Fb
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
    (fun ab => forall x : R, Rmin (fst ab) (snd ab) <= x <= Rmax (fst ab) (snd ab) -> ex_derive f x)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  -> filter_prod Fa Fb
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
    (fun ab => forall x : R, Rmin (fst ab) (snd ab) <= x <= Rmax (fst ab) (snd ab) -> continuous (Derive f) x)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  -> filterlim f Fa (locally la) -> filterlim f Fb (locally lb)
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  -> is_RInt_gen (Derive f) Fa Fb (lb - la).
Proof.
intros Df Cf Lfa Lfb P HP.
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
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.
(* Goal: @ex_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) *)
  by apply filterlim_snd.
  eapply filterlim_comp, @filterlim_opp.
  eapply filterlim_comp, Lfa.
(* Goal: @ex_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) *)
  by apply filterlim_fst.
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  exact: (filterlim_plus lb (- la)).
  exact HP.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: filter_imp (filter_and _ _ (filter_and _ _ Df Cf) HP').
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => [a b] /= {Df Cf HP HP'} [[Df Cf] HP].
eexists.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: conj HP.
(* Goal: is_RInt_gen (fun y : R => @minus (NormedModule.AbelianGroup R_AbsRing V) (f y) (g y)) Fa Fb (@minus (NormedModule.AbelianGroup R_AbsRing V) lf lg) *)
apply: is_RInt_derive => x Hx.
now apply Derive_correct, Df.
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
exact: Cf.
Qed.

Section Complements_RInt_gen.

Context {V : CompleteNormedModule R_AbsRing}.

(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
Lemma ex_RInt_gen_at_point f a b : @ex_RInt_gen V f (at_point a) (at_point b) <-> ex_RInt f a b.
Proof.
split;  case => I.
(* Goal: forall _ : @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b I, @ex_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) *)
  rewrite is_RInt_gen_at_point => HI.
(* Goal: ex_RInt_gen g Fa Fb *)
  by exists I.
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
rewrite -is_RInt_gen_at_point => HI.
(* Goal: ex_RInt_gen g Fa Fb *)
  by exists I.
Qed.

Lemma RInt_gen_at_point f a b :
(* Goal: forall _ : @is_RInt V f a b l, is_RInt_gen f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) l *)
  ex_RInt f a b -> @RInt_gen V f (at_point a) (at_point b) = RInt f a b.
Proof.
(* Goal: forall _ : @ex_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b, @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
move => Hfint.
(* Goal: @eq (CompleteSpace.sort (CompleteNormedModule.CompleteSpace R_AbsRing V)) (@RInt_gen V f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b)) (@RInt V f a b) *)
apply is_RInt_gen_unique.
(* Goal: @is_RInt_gen (CompleteNormedModule.NormedModule R_AbsRing V) f (@at_point R_UniformSpace a) (@at_point R_UniformSpace b) (@RInt V f a b) *)
apply is_RInt_gen_at_point.
(* Goal: @is_RInt (CompleteNormedModule.NormedModule R_AbsRing V) f a b (@RInt V f a b) *)
exact: RInt_correct.
Qed.

End Complements_RInt_gen.
