proposition: Lemma domU (c : R) (x : K) : c != 0 -> dom << c *g x >> = [:: x].
proof: Proof. move=> nz_c; apply/perm_small_eq/uniq_perm => //; first exact: uniq_dom. move=> y; rewrite mem_dom coeffU mem_seq1. by case: (eqVneq x); rewrite /= ?(mulr0, mulr1, eqxx). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)