proposition: Lemma mulmx_rV_of_nat_row m (M : 'M_(n, m)) (k : 'I_n) : rV_of_nat n (expn 2 k) *m M = row (Ordinal (rev_ord_proof k)) M.
proof: Proof. rewrite /rV_of_nat. apply/rowP => i. rewrite !mxE /=. transitivity (\sum_(j < n) (F2_of_bool (nth false (bitseq_of_nat (expn 2 k) n) j) * M j i)). apply eq_bigr => l _; by rewrite mxE. rewrite bitseq_of_nat_expn2 //. set j := Ordinal _. rewrite (bigD1 j) //=. set x := nth _ _ _. have -> : x = true by rewrite /x nth_cat size_nseq ltnn subnn. rewrite mul1r. rewrite [X in _ + X = _](_ : _ = 0) ?addr0 //. rewrite (eq_bigr (fun=> 0)) ?big_const ?iter_addr0 // => l lj. rewrite (_ : nth _ _ _ = false) ?mul0r //. rewrite nth_cat size_nseq. case: ifP => lnk; first by rewrite nth_nseq lnk. rewrite (_ : true :: _ = [:: true] ++ nseq k false) // nth_cat /=. case: ifP => lnk1; last by rewrite nth_nseq; case: ifP. exfalso. clear -lnk1 lj lnk. have {lnk1} : l <= n - k.+1 by rewrite ltnS leqn0 in lnk1. rewrite leq_eqVlt lnk orbC /=; by apply/negP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext mathcomp(bigop zmodp ssralg matrix) ssralg_ext f2