proposition: Lemma row_to_seq_0 n : tuple_of_row 0 = [tuple of nseq n ( 0 : 'F_2)].
proof: Proof. apply eq_from_tnth => i. by rewrite {2}/tnth nth_nseq (ltn_ord i) tnth_mktuple mxE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2