proposition: Lemma precoeff_outdom x s : x \notin predom s -> precoeff x s = 0.
proof: Proof. move=> x_notin_s; rewrite /precoeff big_seq_cond big_pred0 //; case => k z. by apply/contraNF: x_notin_s => /andP[+ /eqP<-]; apply: map_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)