proposition: Lemma sup_Rdown E : sup (Real.down E) == sup E.
proof: Proof. have [supE | trivE] := reals_classic (Real.has_sup E). rewrite /eqR -!sup_sup ?has_sup_Rdown // (ub_Rdown _ _) sup_sup //. by split=> //; rewrite -(ub_Rdown _ _) sup_sup // has_sup_Rdown. by do 2!case: (sup _) / IFR_cases => ? [][]//; rewrite has_sup_Rdown // => _ ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)