proposition: Lemma the_uPath_proof : exists p : Path i o, irred p.
proof: Proof. case/connect_irredP: conn_io => p Ip. by exists p. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)