proposition: Lemma irred_edgeL y x z1 (xz1 : x -- z1) (p : Path z1 y) : irred (pcat (edgep xz1) p) = (x \notin p) && irred p.
proof: Proof. case: p => p pth_p. by rewrite !irredE /= mem_path !nodesE /=. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)