proposition: Theorem FsubnormalDigit : forall p : float, Fsubnormal p -> Fdigit radix p < precision.
proof: Proof. intros p H; unfold Fdigit in |- *. case (Z.eq_dec (Fnum p) 0); intros Z1. rewrite Z1; simpl in |- *; auto with zarith. rewrite Nat.succ_lt_mono, Nat.lt_succ_r. rewrite <- digitPredVNumiSPrecision. replace (S (digit radix (Fnum p))) with (digit radix (Fnum p) + 1). rewrite <- digitAdd; auto with zarith. apply digit_monotone; try assumption. rewrite (fun x => Z.abs_eq (Z.pred x)) by lia. rewrite Zmult_comm; rewrite Zpower_nat_1. generalize (proj2 (proj2 H)); lia. rewrite Nat.add_comm; simpl in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz