fact: Definition OuP (f : A -> R * R -> R) (g : R * R -> R) := { alp : R & { C : R | 0 < alp /\ 0 < C /\ forall X : A, forall dX : R * R, sqrt (Rsqr (fst dX) + Rsqr (snd dX)) < alp -> P dX -> Rabs (f X dX) <= C * Rabs (g dX)}}.
imports: Reals Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice fintype bigop order ssralg ssrnum) mathcomp(boolp reals Rstruct ereal) mathcomp(classical_sets signed topology normedtype landau)