proposition: Lemma can_irred_of : cancel upath_of irred_of.
proof: Proof. (do 2 case) => p ? ?. by do 2 apply: val_inj. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)