proposition: Lemma interiorW p z : z \in interior p -> z \in p.
proof: Proof. rewrite !inE. case: (_ \in _) => //. by rewrite andbF. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)