proposition: Lemma mem_cap_interval xz1 xz2 y : cap_interval xz1 xz2 y <-> xz1 y /\ xz2 y.
proof: Proof. by case: xz1 xz2 => x1 z1 [x2 z2] /=; rewrite ltR_max ltR_min; tauto. 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)