proposition: Theorem Zpos_digits2_pos : forall m : positive, Zpos (digits2_pos m) = Zdigits radix2 (Zpos m).
proof: Proof. intros m. rewrite <- Z_of_nat_S_digits2_Pnat. unfold Z.of_nat. apply f_equal. induction m ; simpl ; try easy ; apply f_equal, IHm. Qed.
imports: Coq(Lia ZArith Zquot) Zaux