proposition: Lemma freegU_eq0 k x : (<< k *g x >> == 0) = (k == 0).
proof: Proof. apply/eqP/eqP => [/(congr1 (coeff x))|->]; last by rewrite freegU0. by rewrite coeff0 coeffU eqxx mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)