proposition: Lemma irred_edge x y (xy: x -- y) : irred (edgep xy) = (x != y).
proof: Proof. by rewrite irredE nodesE /= inE andbT. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)