proposition: Lemma row_mx_take_drop i v : v = castmx (erefl, subnKC (ltnS' (ltn_ord i))) (row_mx (row_take i v) (row_drop i v)).
proof: Proof. rewrite hsubmxK; apply/rowP => j; rewrite !castmxE /= !cast_ord_id. congr (v ord0 _); exact: val_inj. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2