proposition: Lemma components_pblockP (G : sgraph) (H : {set G}) (x y : G) : reflect (exists p : Path x y, p \subset H) (y \in pblock (components H) x).
proof: Proof. apply: (iffP idP). - case/(pblock_eqvE (@sedge_equiv_in _ _)) => xH yH. wlog xNy : / x != y. { move=> Hyp. case: (altP (x =P y)) => [<- _|]; last exact: Hyp. exists (idp x). apply/subsetP=> z. by rewrite mem_idp => /eqP->. } case/(connect_irredRP xNy) => p _ p_sub. by exists p. - case=> p /subsetP p_sub. rewrite pblock_equivalence_partition. + exact: connectRI p_sub. + exact: sedge_equiv_in. + apply: p_sub; exact: path_begin. + apply: p_sub; exact: path_end. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)