proposition: Lemma interiorN p z : z \in interior p -> z \notin [set x; y].
proof: Proof. rewrite inE. by case (_ \in _). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)