proposition: Theorem FnormalPrecision : forall p : float, Fnormal p -> Fdigit radix p = precision.
proof: Proof. intros p H; apply Nat.le_antisymm. apply pGivesDigit; apply H. apply le_S_n. rewrite <- digitVNumiSPrecision. unfold Fdigit in |- *. replace (S (digit radix (Fnum p))) with (digit radix (Fnum p) + 1). rewrite <- digitAdd; auto with zarith. apply digit_monotone; try auto. rewrite (fun x => Z.abs_eq (Zpos x)); auto with zarith. rewrite Zmult_comm; rewrite Zpower_nat_1; auto with zarith. apply H. destruct H as (H1,H2). intros H3; contradict H2; rewrite H3. lia. rewrite Nat.add_comm; simpl in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz