proposition: Lemma Rcondcomplete E : has_sup E -> {m | isLub E m}.
proof: Proof. move=> [E0 uE]; have := completeness E; rewrite boundE => /(_ uE E0)[x [E1 E2]]. exists x; split; first by rewrite -is_upper_boundE; apply: E1. by move=> y; rewrite -is_upper_boundE => /E2/RleP. 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