proposition: Lemma interior_idp (G : sgraph) (x : G) : interior (idp x) = set0.
proof: Proof. apply/setP => z. rewrite !inE mem_idp. by (case: (_ == _)). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)