proposition: Lemma union_merge_r: F ⊎ merge_seq G l ≃ merge_seq (F ⊎ G) (map_pairs unr l).
proof: Proof. eapply iso_comp. apply union_C. eapply iso_comp. apply union_merge_l. eapply iso_comp. apply (merge_iso (union_C _ _)). apply merge_same. abstract by rewrite map_map_pairs. Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)