proposition: Lemma connect_irredP x y : reflect (exists p : Path x y, irred p) (connect (--) x y).
proof: Proof. apply: (iffP (upathP _ _)) => [[p /andP [U P]]|[p I]]. + exists (Sub p P). by rewrite /irred nodesE. + exists (val p). apply/andP;split; by [rewrite /irred nodesE in I| exact: valP]. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)