proposition: Lemma mem_sep_interval x1 x2 : sep_interval x1 x2 x2.
proof: Proof. rewrite /sep_interval; move: {x1}(_ / 2) => y; split. by case: IFR_cases => _ [][lex2y ->] //; apply: ltPR. by case: IFR_cases => _ [][leyx2 ->] //; apply: ltRS. 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)