proposition: Lemma flip_edge_iso (G : pre_graph) (isG : is_graph G) e : pack G ≃2 pack (flip_edge G e).
proof: Proof. iso2 bij_id bij_id (fun e' : edge (pack G) => val e' == e). 2-3: by apply: val_inj. split => //=. - move => e' b. apply/val_inj => /=. case: (altP (fsval e' =P e)) => /= [->|?]; by rewrite updateE. - move => e'. case: (altP (fsval e' =P e)) => /= [->|?]; by rewrite 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)