proposition: Lemma in_eqv_update (aT : choiceType) (rT : Type) (f g : aT -> rT) (E : relation rT) (z : aT) (u v : rT) (A : {fset aT}) : {in A, forall x : aT, E (f x) (g x)} -> E u v -> {in z |` A, forall x : aT, E (f[upd z := u] x) (g[upd z := v] x)}.
proof: Proof. move => H Euv k. rewrite !inE. case: (altP (k =P z)) => [-> _|? /= inA]; rewrite !updateE //. exact: H. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries)