proposition: Theorem digits2_Pnat_correct : forall n, let d := digits2_Pnat n in (Zpower_nat 2 d <= Zpos n < Zpower_nat 2 (S d))%Z.
proof: Proof. intros n d. unfold d. clear. assert (Hp: forall m, (Zpower_nat 2 (S m) = 2 * Zpower_nat 2 m)%Z) by easy. induction n ; simpl digits2_Pnat. rewrite Zpos_xI, 2!Hp. lia. rewrite (Zpos_xO n), 2!Hp. lia. now split. Qed.
imports: Coq(Lia ZArith Zquot) Zaux