proposition: Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Pos.pred p)))%Z.
proof: Proof. intros p; case (Pos.succ_pred_or p); intros H1. subst; simpl plength. rewrite Z.pow_1_r; auto with zarith. pattern p at 1; rewrite <- H1. rewrite Pos2Z.inj_succ; unfold Z.succ. generalize (plength_correct (Pos.pred p)); auto with zarith. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic