proposition: Lemma update_same (aT : eqType) (rT : Type) (f : aT -> rT) x a b : f[upd x := a][upd x := b] =1 f[upd x := b].
proof: Proof. rewrite /update => z. by case: (z == x). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)