proposition: Lemma rev7_bin : forall m, (2 < m)%nat -> rev (bitseq_of_N (BinNums.Npos (xOs (m - 3) (BinNums.xI 3)))) = true :: true :: true :: nseq (m - 3) false.
proof: Proof. elim=> //. case=> //. case=> //. case=> // m /(_ isT). rewrite -{1}addn3 -addnBA // subnn addn0 => IH _. rewrite -{1}addn4 -addnBA //= (_ : 4 - 3 = 1)%nat // addn1 /=. by rewrite rev_cons IH /= -{1}addn3 -addnBA // subnn addn0 -nseq_S. 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