proposition: Lemma Zpower2_Psize n p : Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat.
proof: Proof. revert p; induction n as [|n IHn]. - intros p; destruct p; now split. - assert (Hn := Nat2Z.is_nonneg n). intros p; destruct p as [p|p|]; simpl Pos.size_nat. + specialize IHn with p. rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. + specialize IHn with p. rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. + split. * lia. * intros _. apply Z.pow_gt_1. -- easy. -- now rewrite Nat2Z.inj_succ, Z.lt_succ_r. Qed.
imports: ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory Zpower