proposition: Lemma size_bitseq_of_N_ub' : forall i n, nat_of_bin i <> O -> nat_of_bin i < 2 ^ n -> size (bitseq_of_N i) <= n.
proof: Proof. case=> //=. elim => [p IHp n _ H /= | p IHp n _ H /= | [] //]. - case: n H => [//|n H]. have X : nat_of_pos p < 2 ^ n. have {H} : (nat_of_pos p).*2 < 2 ^ n.+1. rewrite /= NatTrec.doubleE in H. by apply leq_ltn_trans with (nat_of_pos p).*2.+1. by rewrite expnSr muln2 ltn_double. apply IHp in X; last exact: nat_of_pos_not_0. by apply leq_ltn_trans with n. - case: n H => [H|n H]. + rewrite expn0 in H. have {H} : nat_of_pos (BinPos.xO p) = O. by destruct (nat_of_pos (BinPos.xO p)). by move: (@nat_of_pos_not_0 (BinPos.xO p)). + have : nat_of_pos p < 2 ^ n. by rewrite /= NatTrec.doubleE expnSr muln2 ltn_double in H. rewrite ltnS; move/IHp; apply. exact: nat_of_pos_not_0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext