proposition: Fact lt_is_cut a : is_cut {b | a < b}%R.
proof: Proof. split=> [||b c /lt_trans| b /midf_lt[ltac ltcb]]; last 2 [exact]. - by exists (a + 1)%R; rewrite ltr_addl. - by exists a; rewrite ltxx. by exists ((a + b) / 2%:R)%R. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)