proposition: Lemma mem_augment s z x y : x != y -> y \notin (predom s) -> y \notin predom (augment s z x).
proof: Proof. move=> neq_xy; elim: s => [_|[z' x'] s IHs] /=. by rewrite mem_seq1 eq_sym. rewrite in_cons => /norP[neq_yx' Hys]. have [->|neq_xx'] /= := eqVneq x x'. by rewrite in_cons negb_or neq_yx'. by rewrite in_cons negb_or neq_yx' IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)