proposition: Lemma rev_bitseq_of_nat_7 n : (2 < n)%nat -> rev (bitseq_of_nat 7 n) = bitseq_of_nat (7 * expn 2 (n - 3)) n.
proof: Proof. move=>Hn. rewrite /bitseq_of_nat. rewrite (bin_of_nat_rev7 Hn). rewrite (@bin_of_nat_7 n) //=. rewrite (rev7_bin Hn) /=. rewrite {1}/pad_seqL /=. rewrite Hn. rewrite rev_cat /=. rewrite /pad_seqL /=. rewrite size_nseq. case: ifP => H //. rewrite (_ : n - (n - 3).+3 = 0)%nat //; last first. destruct n => //. destruct n => //. destruct n => //. rewrite -addn3. by rewrite -(@addnBA n 3 3) // subnn addn0 addn3 subnn. by rewrite rev_nseq. exfalso. move/negbT in H. rewrite -leqNgt in H. destruct n => //. destruct n => //. destruct n => //. by rewrite -{2}addn3 -addnBA // subnn addn0 ltnn in H. 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