proposition: Lemma is_upper_boundE E x : is_upper_bound E x = (ubound E) x.
proof: Proof. rewrite propeqE; split; [move=> h|move=> /ubP h y Ey; exact/RleP/h]. by apply/ubP => y Ey; apply/RleP/h. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun Zwf Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def Rtrigo1 Reals mathcomp(all_ssreflect ssralg poly mxpoly ssrnum) HB(structures) mathcomp(boolp classical_sets) reals