proposition: Lemma edge_diso F G (h: diso F G) x y: h x -- h y = x -- y.
proof: Proof. apply/idP/idP; last exact: diso_hom. move/(diso_hom' h). by rewrite 2!bijK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)