proposition: Lemma Diso' [F G : diGraph] [f : F -> G] [g : G -> F] : cancel f g -> cancel g f -> {mono f : x y / x -- y} -> F ≃ G.
proof: Proof. move => can_f can_g mono_f. exists (Bij can_f can_g) => /= x y; first abstract by rewrite mono_f. abstract by rewrite -{1}[x]can_g -{1}[y]can_g mono_f. Defined.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)