proposition: Lemma formZl a u v : '[a *: u, v] = a * '[u, v].
proof: Proof. by do !rewrite /form -[_ *: _ *m _]/(mulmxr _ _) linearZ /=; rewrite mxE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)