proposition: Lemma irred_edgeR y x z (yz : y -- z) (p : Path x y) : irred (pcat p (edgep yz)) = (z \notin p) && irred p.
proof: Proof. rewrite !irredE !mem_path !nodesE /= cats1 rcons_uniq mem_rcons !inE. rewrite eq_sym !negb_or. case: (x \notin pval p); by rewrite andbA. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)