proposition: Lemma row_of_seqK n l H f b : map f l = tuple_of_row (@row_of_seq f b l n H).
proof: Proof. apply/(@eq_from_nth _ (f b)) => [|i Hi]. by rewrite size_map size_tuple (eqP H). rewrite size_map in Hi. rewrite (nth_map b) //. rewrite (eqP H) in Hi. transitivity (tnth (tuple_of_row (row_of_seq f b H)) (Ordinal Hi)). by rewrite tnth_mktuple mxE. 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