proposition: Lemma connect_irredRP {A : pred D} x y : x != y -> reflect (exists2 p: Path x y, irred p & p \subset A) (connect (restrict A (--)) x y).
proof: Proof. move => Hxy. apply: (iffP connect_restrictP) => //. - case => p [pth_p lst_p uniq_p sub_A]. have pvalP : pathp x y p by rewrite /pathp pth_p lst_p. exists (Build_Path pvalP); first by rewrite irredE nodesE. apply/subsetP => z. rewrite mem_path nodesE. exact: sub_A. - case => p Ip /subsetP subA; exists (val p). by case/andP : (valP p) => ? /eqP ?; rewrite -nodesE -irredE. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)