proposition: Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z.
proof: Proof. assert (F: (forall p, 2 ^ (Zpos (Pos.succ p)) = 2 * 2 ^ Zpos p)%Z). intros p; replace (Zpos (Pos.succ p)) with (1 + Zpos p)%Z. rewrite Zpower_exp; auto with zarith. rewrite Pos2Z.inj_succ; unfold Z.succ; auto with zarith. intros p; elim p; simpl plength; auto. intros p1 Hp1; rewrite F; repeat rewrite Pos2Z.inj_xI. rewrite <- !Z.add_diag; auto with zarith. intros p1 Hp1; rewrite F; rewrite (Pos2Z.inj_xO p1). rewrite <- !Z.add_diag; auto with zarith. rewrite Z.pow_1_r; auto with zarith. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic