proposition: Theorem pos_length_pow : forall p : positive, (Zpos p < Zpower_nat n (S (pos_length p)))%Z.
proof: Proof. intros p; elim p; simpl in |- *. 3: lia. intros p0 H; rewrite Zpos_xI. apply Z.lt_le_trans with (2 * (n * Zpower_nat n (pos_length p0)))%Z; try lia. apply Zmult_le_compat_r; lia. intros p0 H; rewrite Zpos_xO. apply Z.lt_le_trans with (2 * (n * Zpower_nat n (pos_length p0)))%Z; try lia. apply Zmult_le_compat_r; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz