proposition: Lemma irredxx (x : G) (p : Path x x) : irred p -> p = idp x.
proof: Proof. rewrite irredE /tail (lock uniq); case: p => p p_pth /=. rewrite nodesE /= -lock => p_uniq. apply/val_inj => /=. by have /upath_nil-> : upath x x p by rewrite /upath p_uniq p_pth. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)