proposition: Lemma irred_cat : irred (pcat p q) = [&& irred p, irred q & [set u : D in p | u \in q] == [set y]].
proof: Proof. rewrite /irred {1}nodesE (lock uniq) /= -lock -cat_cons -nodesE cat_uniq. congr (_ && _). rewrite (nodesE q) /=. case: uniq => //; rewrite !andbT. apply/hasPn/andP. - move=> H. split; first by apply/negP=>/H/=; rewrite path_end. apply/eqP/setP=> u; rewrite !inE. apply/andP/eqP; last by [move=>->; rewrite path_begin path_end]. case=> u_p. rewrite mem_path nodesE inE =>/orP[/eqP//|/H/=]. by rewrite u_p. - case=> zNTq. rewrite eqEsubset =>/andP[/subsetP sub _]. move=> u u_q /=. apply/negP=> u_p. case/(_ u _)/Wrap: sub; rewrite inE. + rewrite u_p /=; exact: tailW. + apply/negP; by apply: contraNneq zNTq =>{1}<-. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)