proposition: Lemma IFR_cases : selectR_spec (IF P then x else y).
proof: Proof. have [z Ez]: Real.nonempty E. by have [haveP | notP] := decP; [exists x; left | exists y; right]. have Dz t: E t <-> t == z. by case: Ez => -[defP ->]; do [split=> [[][]|]; last by [left | right]]. have le_E_z: Real.ub E z by move=> _ /Dz->. have supE: Real.has_sup E by split; exists z. by split; apply/Dz; split; [apply: real_sup_le_ub | apply: real_sup_ub]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)