proposition: Lemma meet_sep_interval x y t : sep_interval x y t -> sep_interval y x t -> x == y.
proof: Proof. without loss ltxy: x y / x < y. by move=> IHxy ? ?; have [|/ltR_total[]/IHxy->] := reals_classic R (x == y). case; set u := (x + y) / 2 => /ltRW-lttu _ [_ []]; rewrite addRC. suffices{lttu} [ltxu ltuy]: x < u < y by rewrite !IFR_else in lttu *. have Du: 2 * u == x + y by rewrite [u]mulRC mulRCA pmulKR. by split; rewrite -(leR_pmul2l _ _ ltR02) Du mul2R (leR_add2l, leR_add2r). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple path fingraph bigop order ssralg) mathcomp(ssrnum ssrint div intdiv) fourcolor(hypermap geometry coloring grid matte) fourcolor(real realplane) Coq(Setoid Morphisms) fourcolor(realsyntax realprop)