proposition: Lemma vecof_linear : linear vecof.
proof: Proof. move=> x v1 v2; rewrite linear_sum -big_split/=. by apply: eq_bigr => i _/=; rewrite !mxE scalerDl scalerA. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)