proposition: Lemma merge_add_vertexLE x: merge_add_vertexL (\pi (inl x)) = match x with inl x => inl (\pi inl x) | _ => inr tt end.
proof: Proof. simpl. rewrite (@merge_isoE _ _ _ _ (iso_sym (union_A G (unit_graph a) H)) l). rewrite (@merge_isoE _ _ _ _ (union_iso iso_id (union_C (unit_graph a) H)) _). rewrite (@merge_isoE _ _ _ _ (union_A G H (unit_graph a)) _). rewrite merge_same'E. rewrite union_merge_lE'. by case x=>[y|[]]. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)