proposition: Lemma tuple_of_row_row_mx (C : finType) n1 n2 (v1 : 'rV[C]_n1) (B : 'rV[C]_n2) : tuple_of_row (row_mx v1 B) = [tuple of tuple_of_row v1 ++ tuple_of_row B].
proof: Proof. apply eq_from_tnth => n0. rewrite tnth_mktuple mxE. case: splitP => [n3 n0n3|n3 n0n1n3]. rewrite /tnth nth_cat size_tuple (_ : (n0 < n1 = true)%nat); last by rewrite n0n3 ltn_ord. transitivity ((tuple_of_row v1) !_ n3); first by rewrite tnth_mktuple. rewrite /tnth n0n3; apply set_nth_default; by rewrite size_tuple. rewrite /tnth nth_cat size_tuple (_ : (n0 < n1 = false)%nat); last first. rewrite n0n1n3; apply/negbTE; by rewrite -leqNgt leq_addr. transitivity ((tuple_of_row B) !_ n3); first by rewrite tnth_mktuple. rewrite /tnth (_ : (n0 - n1 = n3)%nat); last by rewrite n0n1n3 addnC addnK. apply set_nth_default; by rewrite size_tuple. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2