proposition: Lemma merge_surj: merge G r ≃ H.
proof: Proof. Iso (quot_kernel Hr Hsurj) fe fd. split; intros=>/=. - by rewrite (endpoint_hom (is_hom := Hhom)) quot_kernelE. - rewrite vlabel_hom. apply: eqv_bigl => x. apply/eqP/eqP => E. * move:E=>/Hr/eqquotP E. rewrite E. apply reprK. * by rewrite -E quot_kernelE. - exact:(elabel_hom (is_hom := Hhom)). Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)