proposition: Lemma open_add_edge (x y : G) u : open (G ∔ [x, u, y]) ⩭2 open G ∔ [inj_v x, u, inj_v y].
proof: Proof. have X : is_graph (add_edge (open G) (inj_v x) u (inj_v y)). { exact: add_edge_graph. } econstructor. apply: iso2_comp (iso2_sym _) _. apply: openK. apply: iso2_comp _ (iso2_sym _). 2: apply pack_add_edge. apply: (add_edge2_iso'' (h := (openK _))) => //; exact: openKE. Defined.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)