proposition: Lemma val_genK : cancel val_gen in_gen.
proof: Proof. move=> W; apply/matrixP=> i j; apply: val_inj; rewrite mxE /= rowK. case/row_freeP: base_free => B' BB'; rewrite -[_ *m _]mulmx1 -BB' mulmxA. by rewrite mulmxKpV ?submxMl // -mulmxA BB' mulmx1 mxvecK rowK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)