proposition: Lemma irred_catD : irred (pcat p q) = [&& irred p, irred q & [disjoint p & tail q]].
proof: Proof. rewrite /irred {1}/nodes -lock /pcat SubK -cat_cons cat_uniq. rewrite -disjoint_has disjoint_sym -nodesE. case A : [disjoint _ & _] => //. case: (uniq (nodes p)) => //=. rewrite nodesE /=. case: (uniq _) => //=. by rewrite !andbT (disjointFr A _) // path_end. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)