proposition: Lemma freeg_muln k n (S : K) : << k *g S >> *+ n = << (k *+ n) *g S >>.
proof: Proof. elim: n => [|n ih]. + by rewrite !mulr0n freegU0. + by rewrite !mulrS ih freegUD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)