proposition: Lemma precoeff_mem_uniqE s kz : uniq (predom s) -> kz \in s -> precoeff kz.2 s = kz.1.
proof: Proof. move=> uniq_dom_s kz_in_s; have uniq_s := map_uniq uniq_dom_s. rewrite precoeff_uniqE // (nth_map kz); last first. by rewrite -(size_map (@snd _ _)) index_mem map_f. rewrite nth_index_map // => {kz kz_in_s} kz1 kz2 kz1_in_s kz2_in_s eq. apply/eqP. rewrite -[kz1](nth_index kz1 (s := s)) // -[kz2](nth_index kz1 (s := s)) //. rewrite nth_uniq ?index_mem // -(nth_uniq kz1.2 (s := predom s)) //; try by rewrite size_map index_mem. by rewrite !(nth_map kz1) ?index_mem // !nth_index // eq eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)