proposition: Lemma sup_le_ub {E} x : E !=set0 -> (ubound E) x -> sup E <= x.
proof: Proof. move=> hasE leEx; set y := sup E; pose z := (x + y) / 2%:R. have Dz: 2%:R * z = x + y. by rewrite mulrCA divff ?mulr1 // pnatr_eq0. have ubE : has_sup E by split => //; exists x. have [/downP [t Et lezt] | leyz] := sup_total z ubE. rewrite -(lerD2l x) -Dz -mulr2n -[leRHS]mulr_natl. rewrite ler_pM2l ?ltr0Sn //; apply/(le_trans lezt). by move/ubP : leEx; exact. rewrite -(lerD2r y) -Dz -mulr2n -[leLHS]mulr_natl. by rewrite ler_pM2l ?ltr0Sn. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid