proposition: Theorem pNormal_absolu_min : forall p : float, Fnormal p -> (nNormMin <= Z.abs (Fnum p))%Z.
proof: Proof. intros p H; apply Zmult_le_reg_r with (p := radix); auto with zarith. unfold nNormMin in |- *. pattern radix at 2 in |- *; rewrite <- (Zpower_nat_1 radix). rewrite <- Zpower_nat_is_exp; auto with zarith. replace (pred precision + 1) with precision. rewrite <- pGivesBound. rewrite <- (Z.abs_eq radix); auto with zarith. rewrite <- Zabs_Zmult; rewrite Zmult_comm; apply H. lia. Qed.
imports: Reals ZArith List PeanoNat Psatz