proposition: Lemma add_edge_rev F x u v y (e: u ≡' v): F ∔ [x, u, y] ≃ F ∔ [y, v, x].
proof: Proof. Iso bij_id bij_id (fun x => match x with Some _ => false | None => true end). abstract (split; (repeat case)=>//=; by apply Eqv'_sym). Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)