proposition: Lemma add_testC (G : pre_graph) x y a b : G[adt x <- a][adt y <- b] ≡G G[adt y <- b][adt x <- a].
proof: Proof. split => //= z. case: (altP (x =P y)) => xy; subst. - rewrite !update_same. case: (altP (z =P y)) => zy; subst; rewrite !updateE => //=. by rewrite monA [(b ⊗ a)%CM]monC -monA. - case: (altP (z =P x)) => zx; case: (altP (z =P y)) => zy; subst. by rewrite eqxx in xy. all: by rewrite !updateE. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)