proposition: Theorem digitnNormMin : digit radix nNormMin = precision.
proof: Proof. unfold nNormMin, Fdigit in |- *; simpl in |- *; apply digitInv; try assumption. rewrite Z.abs_eq; try apply Zpower_NR0; auto with zarith. rewrite Z.abs_eq; try apply Zpower_NR0; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz