proposition: Lemma precoeff_uniqE s x : uniq (predom s) -> precoeff x s = [seq v.1 | v <- s]`_(index x (predom s)).
proof: Proof. elim: s => [|[z y s ih]]; first by rewrite precoeff_nil nth_nil. rewrite precoeff_cons /= => /andP [x_notin_s /ih ->]. have [->|ne_yx] := eqVneq x y; last by rewrite mul0r add0r. by rewrite mul1r /= nth_default ?addr0 // memNindex //= !size_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)