proposition: Lemma bin_of_nat_rev7 : forall n, 2 < n -> bin_of_nat (7 * 2 ^ (n - 3)) = BinNums.Npos (xOs (n - 3) (BinNums.xI (BinNums.xI (BinNums.xH)))).
proof: Proof. elim=> //. case=> //. case=> //. case=> //. move=> n /(_ Logic.eq_refl) => IH _. rewrite (_ : n.+4 - 3 = n.+1)%nat //. rewrite (_ : n.+3 - 3 = n)%nat // in IH; last by rewrite 3!subSS subn0. transitivity (BinNat.N.mul 2 (bin_of_nat (7 * 2 ^ n))); last by rewrite {}IH -BinPos.Pos.add_diag. set lhs := bin_of_nat _. set rhs := BinNat.N.mul _ _. suff : nat_of_bin lhs = nat_of_bin rhs. rewrite {1}/lhs bin_of_natK /lhs => ->. by rewrite nat_of_binK. rewrite /lhs /rhs bin_of_natK nat_of_mul_bin expnS mulnA (mulnC 7) -mulnA. f_equal. by rewrite bin_of_natK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext