fact: Definition Rneg_over (g : R -> R) := forall x : R, (P x -> g x <= 0)%R.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor