proposition: Lemma p''GivesBound: Zpos (vNum bt)=(Zpower_nat radix s).
proof: Proof. clear -radixMoreThanOne. unfold bt in |- *; unfold vNum in |- *. apply trans_eq with (Z_of_nat (nat_of_P (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix s)))))). unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with zarith. rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith. cut (Z.abs (Zpower_nat radix s) = Zpower_nat radix s). intros H; pattern (Zpower_nat radix s) at 2 in |- *; rewrite <- H. rewrite Zabs_absolu. rewrite (Nat.lt_succ_pred 0 (Z.abs_nat (Zpower_nat radix s))); auto with arith zarith. apply lt_Zlt_inv; simpl in |- *; auto with zarith arith. rewrite <- Zabs_absolu; rewrite H; auto with arith zarith. apply Zpower_nat_less; lia. apply Z.abs_eq; auto with arith zarith. apply Zpower_NR0; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz