proposition: Lemma OuO_to_P f g : OuO f g -> OuP f g.
proof: Proof. move=> fOg; apply/Ouex_to_P; move: fOg => /eqOP [k [kreal hk]]. have /hk [Q [->]] : k < maxr 1 (k + 1) by rewrite lt_maxr ltrDl orbC ltr01. move=> [R [[_/posnumP[e1] Re1] [_/posnumP[e2] Re2]] sRQ] fOg. exists (minr e1%:num e2%:num) => //. exists (maxr 1 (k + 1)); first by rewrite lt_maxr ltr01. move=> x dx dxe Pdx; apply: (fOg (x, dx)); split=> //=. move: dxe; rewrite lt_maxl !lt_minr => /andP[/andP [dxe11 _] /andP [_ dxe22]]. by apply/sRQ => //; split; [apply/Re1|apply/Re2]; rewrite /= distrC subr0. 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)