proposition: Theorem Z_of_nat_S_digits2_Pnat : forall m : positive, Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).
proof: Proof. intros m. apply eq_sym, Zdigits_unique. rewrite <- Zpower_nat_Z. rewrite Nat2Z.inj_succ. change (_ - 1)%Z with (Z.pred (Z.succ (Z.of_nat (digits2_Pnat m)))). rewrite <- Zpred_succ. rewrite <- Zpower_nat_Z. apply digits2_Pnat_correct. Qed.
imports: Coq(Lia ZArith Zquot) Zaux