proposition: Lemma isubgraph_iso (F G : diGraph) (i : F ⇀ G) : #|G| <= #|F| -> F ≃ G.
proof: Proof. move: i => [f inj_f mono_f] leqGF. have onto_f : forall y, y \in codom f by apply: inj_card_onto. pose g (y : G) : F := iinv (onto_f y). have can_f : cancel f g by abstract by move => x; rewrite /g iinv_f. have can_g : cancel g f by abstract by move => x; rewrite /g f_iinv. exact: Diso' can_f can_g mono_f. Defined.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)