proposition: Lemma connected_interior (G : sgraph) (x y : G) (p : Path x y) : irred p -> connected (interior p).
proof: Proof. case: (altP (x =P y)) => [?|xNy] Ip; subst. - rewrite (irredxx Ip) interior_idp. exact: connected0. - case: (splitL p xNy) => x' [xx'] [p'] [E _]. rewrite E irred_edgeL in Ip. case/andP : Ip => xp Ip'. case: (altP (x' =P y)) => [?|x'Ny]; subst. + rewrite (irredxx Ip') pcat_idR interior_edgep. exact: connected0. + case: (splitR p' x'Ny) => z [q] [zy] ?. subst. rewrite irred_edgeR in Ip'. case/andP : Ip' => yq Iq. suff -> : interior (pcat (edgep xx') (pcat q (edgep zy))) = [set u in q]. { exact: connected_path. } apply/setP => u. rewrite 3!inE mem_pcat_edgeL mem_pcat_edgeR !inE. case: (u =P x) => [ux|_];case: (u =P y) => [uy|_] => //=; subst u. all: rewrite ?(negbTE yq) //; symmetry. all: by apply: contraNF xp; rewrite !inE => ->. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)