proposition: Lemma OuP_to_O f g : OuP f g -> OuO f g.
proof: Proof. move=> /OuP_to_ex [_/posnumP[a] [_/posnumP[C] fOg]]. apply/eqOP; near=> k; near=> x; apply: le_trans (fOg _ _ _ _) _; last 2 first. - by near: x; exists (setT, P); [split=> //=; apply: withinT|move=> ? []]. - by rewrite ler_pM. - near: x; exists (setT, ball (0 : R^o * R^o) a%:num). by split=> //=; rewrite /within /=; near=> x =>_; near: x; apply: nbhsx_ballx. move=> x [_ [/=]]; rewrite -ball_normE /= distrC subr0 distrC subr0. by move=> ??; rewrite lt_maxl; apply/andP. Unshelve. all: by end_near. 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)