proposition: Lemma bitseq_row_nth n (i j : bitseq) : (size i <= n)%nat -> size i = size j -> \row_(k < n) F2_of_bool (nth false i k) = \row_(k < n) F2_of_bool (nth false j k) -> i = j.
proof: Proof. move=> ni ij /rowP h; apply/(@eq_from_nth _ false _ _ ij) => k kj. have kn : (k < n)%nat by rewrite (leq_trans kj)// ji. by move: (h (Ordinal kn)); rewrite !mxE /=; do 2 case: nth. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)