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