proposition: Lemma add_edge_flip (G : pre_graph) e x y u v (isG1 : is_graph (G ∔ [e,x,u,y])): u° ≡ v -> x \in vset G -> y \in vset G -> G ∔ [e,x,u,y] ⩭2 G ∔ [e,y,v,x].
proof: Proof. move => E xG yG. have isG2 : is_graph (G ∔ [e,y,v,x]) by apply: add_edge_graph''. econstructor. pose dir (e0 : edge (pack (G ∔ [e,x,u,y]) isG1)) := val e0 == e. iso2 bij_id bij_id dir => //=. 2-3: exact: val_inj. split => //. - case => e' He' b /=. apply: val_inj => /=. case: (fset1UE He') => [?|]. + subst e'. by rewrite /dir/=!eqxx addTb !updateE if_neg. + case => A ?. by rewrite /dir/= (negbTE A) !updateE. - case => e' He'. rewrite /dir/=. case: (fset1UE He') => [?|]. + subst e'. rewrite eqxx !updateE. by symmetry in E. + case => A ?. by rewrite /dir/= (negbTE A) !updateE. 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)