proposition: Lemma is_RInt_gen_swap {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb} (f : R -> V) (l : V) : is_RInt_gen f Fb Fa l -> is_RInt_gen f Fa Fb (opp l).
proof: Proof. intros Hf P HP. specialize (Hf (fun y => P (opp y))). destruct Hf as [Q R HQ HR H]. exact: filterlim_opp. apply: Filter_prod HR HQ _ => a b Ha Hb. specialize (H b a Hb Ha). destruct H as [y [Hy1 Hy2]]. exists (opp y). split. exact: is_RInt_swap. exact Hy2. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis