proposition: Theorem of_Z_correct: forall p, 0 <= p < base digits -> [|of_Z p|] = p.
proof: Proof. intros p; case p; simpl; try rewrite spec_0; auto. - intros; rewrite of_pos_correct; lia. - intros p1 (H1, _); contradict H1; apply Z.lt_nge; red; simpl; auto. Qed.
imports: ZArith Lia Znumtheory Zpow_facts DoubleType