proposition: Lemma filter_prod_at_point_infty : forall a (P : R -> R -> Prop), (forall x y, a <= x <= y -> P x y) -> filter_prod (at_point a) (Rbar_locally p_infty) (fun ab : R * R => P ab.1 ab.2).
proof: Proof. intros a P HP. apply (Filter_prod _ _ _ (fun x => x = a) (fun x => a < x)). - easy. - now exists a. - move => x y -> /= H. apply HP. split. apply Rle_refl. now apply Rlt_le. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl