proposition: Fact sup_is_cut E : is_cut {a | IF has_sup E then lt_sup E a else 0 < a}.
proof: Proof. split=> [||a b ltEa ltab| a]. - have [supE|] := classical (has_sup E); last by exists 1%R; right. have [_ [x ubEx]] := supE; have [a /open[b ltab ltbx]] := cut_ub x. by exists a; left; split; last by exists b => // y /ubEx/leR_ltc_trans; apply. - have [supE|] := classical (has_sup E); last by exists 0%R => -[][]. have [[y Ey] _] := supE; have [a leay] := cut_lb y. by exists a => -[][] // _ [b ltEb /lt_gec_trans/(_ leay)[]]; apply: ltEb. - case: ltEa => -[supE ltEa]; last by right; rewrite ltcE (lt_trans ltEa). by have [c] := ltEa; left; split=> //; exists c; last apply: lt_trans ltab. case=> -[supE] => [supEa | /open[c]]; last by exists c; first right. have [c ltEc /open[b ltcb ltba]] := supEa. by exists b; first by left; split; last exists c. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)