proposition: Lemma filter_prod_at_point_l : forall {T F} { FF : Filter F} a (P : T -> R -> Prop) Q, F Q -> (forall y, Q y -> P y a) -> filter_prod F (at_point a) (fun ab : T * R => P ab.1 ab.2).
proof: Proof. intros T F FF a P Q FQ HQ. apply: (Filter_prod _ _ _ Q (fun x => x = a)) => // . - move => x y /= H ->. exact: HQ. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl