proposition: Lemma edge_diso' F G (h: diso F G) x y: h^-1 x -- h^-1 y = x -- y.
proof: Proof. apply (edge_diso (diso_sym h)). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)