proposition: Lemma irred_ind P (y : G) : P y y (idp y) -> (forall x z (p : Path z y) (xz : x -- z), irred p -> x \notin p -> P z y p -> P x y (pcat (edgep xz) p)) -> forall x (p : Path x y), irred p -> P x y p.
proof: Proof. move => Hbase Hstep x p. pattern x,y,p. apply: Path_ind => // {x p} x z p xz IH. rewrite irred_edgeL => /andP[A B]. by apply: Hstep; auto. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)