proposition: Fact opp_is_cut x : is_cut (opp_cut x).
proof: Proof. split=> [||a b [c lt_na_c lecx] | a [b /(@open (- a)%R)[c lt_na_c ltcb] lebx]]. - by have [a leax] := cut_lb x; exists (1 - a)%R, a; rewrite // opprB gtr_addl. - have [a ltxa] := cut_ub x; exists (- a)%R => -[b ltab []]. by apply: ltc_trans ltab; rewrite opprK. - by exists c; first by apply: lt_trans lt_na_c; rewrite ltr_opp2. by exists (- c)%R; [exists b; rewrite ?opprK | rewrite ltr_oppl]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)