proposition: Lemma row_of_tuple_inj n : injective (@row_of_tuple n).
proof: Proof. by move=> a b ab; rewrite -(row_of_tupleK b) -ab row_of_tupleK. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2