proposition: Theorem pheight_correct: forall p, Zpos p < 2 ^ (Zpos (ZnZ.digits (dom_op 0)) * 2 ^ (Z.of_nat (pheight p))).
proof: Proof. intros p; unfold pheight. rewrite Nat2Z.inj_pred by apply Pos2Nat.is_pos. rewrite positive_nat_Z. rewrite <- Z.sub_1_r. assert (F2:= (get_height_correct (ZnZ.digits (dom_op 0)) (plength p))). apply Z.lt_le_trans with (Zpos (Pos.succ p)). rewrite Pos2Z.inj_succ; auto with zarith. apply Z.le_trans with (1 := plength_pred_correct (Pos.succ p)). rewrite Pos.pred_succ. apply Z.pow_le_mono_r; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen