proposition: Theorem FnormalPpred : forall x : Z, (- dExp b <= x)%Z -> Fnormal (Float (pPred (vNum b)) x).
proof: Proof. intros x H; (cut (0 <= pPred (vNum b))%Z; [ intros Z1 | unfold pPred in |- *; lia ]). repeat split; simpl in |- *; auto with zarith. rewrite (Z.abs_eq (pPred (vNum b))). unfold pPred in |- *; auto with zarith. unfold pPred in |- *; rewrite pGivesBound; lia. rewrite Zabs_Zmult; repeat rewrite Z.abs_eq; auto with zarith. apply Z.le_trans with ((1 + 1) * pPred (vNum b))%Z; auto with zarith. replace ((1 + 1) * pPred (vNum b))%Z with (pPred (vNum b) + pPred (vNum b))%Z; auto with zarith. replace (Zpos (vNum b)) with (1 + Z.pred (Zpos (vNum b)))%Z; unfold pPred in |- *; auto with zarith. apply Zplus_le_compat_r; apply Zle_Zpred. apply vNumbMoreThanOne. Qed.
imports: Reals ZArith List PeanoNat Psatz