proposition: Lemma precoeffE x : precoeff x =1 prelift (fun y => (y == x)%:R : R^o).
proof: Proof. move=> s; rewrite [RHS](bigID [pred kx | kx.2 == x]) /= addrC big1. by rewrite add0r; apply: eq_bigr => i /eqP ->; rewrite eqxx [_ *: _]mulr1. by move=> i /negbTE ->; rewrite scaler0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)