proposition: Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Pos.pred p)))%Z.
proof: Proof. intros p; case (Psucc_pred p); intros H1. subst; simpl plength. rewrite Zpower_1_r; auto with zarith. pattern p at 1; rewrite <- H1. rewrite Zpos_succ_morphism; unfold Z.succ; auto with zarith. generalize (plength_correct (Pos.pred p)); auto with zarith. Qed.
imports: ZArith Zpow_facts