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. 1-2: auto with zarith. red; intros; discriminate. rewrite Zpos_succ_morphism; unfold Z.succ; auto with zarith. intros p; elim p; simpl plength; auto. intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI. assert (tmp: (forall p, 2 * p = p + p)%Z); try repeat rewrite tmp; auto with zarith. intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1). assert (tmp: (forall p, 2 * p = p + p)%Z); try repeat rewrite tmp; auto with zarith. rewrite Zpower_1_r; auto with zarith. Qed.
imports: ZArith Zpow_facts