proposition: Lemma update_fx (aT : eqType) (rT : Type) (f : aT -> rT) (x : aT): f[upd x := f x] =1 f.
proof: Proof. move => y. rewrite /update. by case: (altP (y =P x)) => [->|]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)