proposition: Lemma real_sup_le_ub E x : Real.has_sup E -> Real.ub E x -> Real.sup E <= x.
proof: Proof. set y := Real.sup E => supE leEx; pose z := (x + y) * Real.inv 2. have le2M := Real.mul_monotone R leR02. have mul2inv: 2 * Real.inv 2 == 1 := Real.mul_inverse_right R (gtR_neq ltR02). have{mul2inv} D2z: 2 * z == x + y by rewrite mulRCA mul2inv mulR1. have [[t /leEx-letx lezt] | leyz] := real_sup_total z supE. by have /le2M := leR_trans lezt letx; rewrite D2z mul2R leR_add2l. by have /le2M := leyz; rewrite D2z mul2R leR_add2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)