proposition: Fact add_is_cut x y : is_cut (add_cut x y).
proof: Proof. split=> [|| a b [c ltxc ltyac] ltab | a [b ltxb /open[c ltyc ltcab]]]. - have [[a ltxa] [b ltyb]] := (cut_ub x, cut_ub y). by exists (b + a)%R, a; rewrite ?addrK. - have [[a leax] [b /leRq-leby]] := (cut_lb x, cut_lb y). exists (b + a)%R => -[c ltxc /leby]. by rewrite ltcE ltr_subr_addr ltr_add2l => /(ltc_trans ltxc). - by exists c => //; apply: ltc_trans ltyac _; rewrite ltr_add2r. by exists (c + b)%R; [exists b; rewrite ?addrK | rewrite -ltr_subr_addr]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)