proposition: Lemma is_RInt_gen_0 {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb} : is_RInt_gen (fun y => 0) Fa Fb zero.
proof: Proof. apply: filterlimi_const. intros [a b]. rewrite -(scal_zero_r (b - a)). exact: is_RInt_const. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl