proposition: Lemma is_RInt_gen_minus {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) (lf lg : V) : is_RInt_gen f Fa Fb lf -> is_RInt_gen g Fa Fb lg -> is_RInt_gen (fun y => minus (f y) (g y)) Fa Fb (minus lf lg).
proof: Proof. intros Hf Hg. apply: is_RInt_gen_plus Hf _. exact: is_RInt_gen_opp. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis