proposition: Lemma union_add_edge_l F G x u y: F ∔ [x, u, y] ⊎ G ≃ (F ⊎ G) ∔ [unl x, u, unl y].
proof: Proof. Iso bij_id (@sum_option_l _ _) xpred0. abstract by split; repeat case. Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)