proposition: Lemma outdom_augmentE s k x : x \notin predom s -> augment s k x = rcons s (k, x).
proof: Proof. elim: s=> [//|[k' x'] s IHs] /=; rewrite in_cons. by case/norP=> /negbTE -> /IHs ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)