proposition: Lemma Ouex_to_P f g : OuPex f g -> OuP f g.
proof: Proof. move=> /exists2P /getPex; set Q := fun a => _ /\ _ => - [lt0getQ]. move=> /exists2P /getPex; set R := fun C => _ /\ _ => - [lt0getR fOg]. apply: existT (get Q) _; apply: exist (get R) _; split=> //; split => //. move=> x dx ltdxgetQ; apply: fOg; apply: le_lt_trans ltdxgetQ. by 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)