proposition: Lemma reduced_mem s k x : reduced s -> ((k, x) \in s) = (precoeff x s == k) && (k != 0).
proof: Proof. elim: s => [|[k' x'] s IHs] /=. by rewrite in_nil precoeff_nil eq_sym andbN. rewrite reduced_cons in_cons precoeff_cons. case/and3P=> [/= nz_k' x'Ns /IHs ->]; rewrite eqE /=. case: (eqVneq x' x) x'Ns => [-> xNs|nz_x's]. rewrite andbT mul1r precoeff_outdom // addr0. by have [->|_] //= := eqVneq k k'; case: eqVneq. by rewrite andbF mul0r add0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)