proposition: Theorem spec_of_pos: forall x, [of_pos x] = Zpos x.
proof: Proof. intros x; unfold of_pos. rewrite spec_reduce. simpl. apply ZnZ.of_pos_correct. unfold base. apply Z.lt_le_trans with (1 := pheight_correct x). apply Z.pow_le_mono_r; auto with zarith. rewrite (digits_dom_op (_ _)), Pshiftl_nat_Zpower. auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen