proposition: Fact pickR_ext (P Q : pred R) : P =1 Q -> pickR P =1 pickR Q.
proof: Proof. move=> PEQ n; rewrite /pickR; set u := epsilon _ _; set v := epsilon _ _. suff->: u = v by rewrite PEQ. by congr epsilon; apply: functional_extensionality=> x; rewrite PEQ. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures)