proposition: Lemma connected_interiorR (G : sgraph) (x y : G) (p : Path x y) : irred p -> connected (y |: interior p).
proof: Proof. move => Ip. case: (set_0Vmem (interior p)) => [->|[z Hz]]. - rewrite setU0. exact: connected1. - apply: neighbor_connected; [exact: connected1|exact: connected_interior|]. apply: path_neighborR => //; by set_tac. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)