proposition: Lemma leR_total x y : x <= y \/ y <= x.
proof: Proof. have ubEy: Real.has_sup {z | z = y} by split; exists y => // _ ->. have [[_ ->] | leEyx] := real_sup_total x ubEy; first by left. right; apply: leR_trans leEyx; apply: real_sup_ub => //; exists y => _ ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)