proposition: Lemma reals_classic : excluded_middle.
proof: Proof. move=> P; have supE: Real.has_sup {x | x = 0 \/ P /\ x = 2 :> R}. by split; [exists 0; left | exists 2 => x [->|[_ ->]]]. have [[x [-> /ltR01 // | []]] | leE1] := real_sup_total 1 supE; first by left. by right=> haveP; apply/(leR_lt_trans leE1 (ltRS 1))/real_sup_ub; last right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)