proposition: Lemma OuP_to_ex f g : OuP f g -> OuPex f g.
proof: Proof. move=> [_ [_ [/posnumP[a] [/posnumP[C] fOg]]]]. exists (a%:num / Num.sqrt 2) => //; exists C%:num => // x dx ltdxa Pdx. apply: fOg; move: ltdxa; rewrite ltr_pdivlMr //; apply: le_lt_trans. by rewrite mulrC; have /andP[] := ler_norm2 dx. Qed.
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)