proposition: Theorem pGivesDigit : forall p : float, Fbounded b p -> Fdigit radix p <= precision.
proof: Proof. intros p H; unfold Fdigit in |- *. rewrite <- digitPredVNumiSPrecision. apply digit_monotone; auto with zarith. rewrite (fun x => Z.abs_eq (Z.pred x)). generalize (proj1 H); auto with zarith. apply Zle_Zpred; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz