proposition: Lemma interior_eq_nodes : interior p = interior q.
proof: Proof. rewrite /interior (_ : [set x in p] = [set x in q]) //. apply/setP => z. by rewrite !inE mem_eq_nodes. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)