proposition: Theorem pheight_correct: forall p, (Zpos p <= 2 ^ (2 ^ (Zpos (pheight p))))%Z.
proof: Proof. intros p; apply Z.le_trans with (1 := (plength_pred_correct p)). apply Zpower_le_monotone; auto with zarith. split; auto with zarith. unfold pheight; apply plength_pred_correct. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod