proposition: Theorem FnormalizeBounded : forall p : float, Fbounded b p -> Fbounded b (Fnormalize p).
proof: Proof. intros p H'; red in |- *; split. unfold Fnormalize in |- *; case (Z_zerop (Fnum p)); try easy. intros H'0. apply digitGivesBoundedNum; auto. rewrite FshiftFdigit; auto. apply Nat.le_trans with (m := Fdigit radix p + (precision - Fdigit radix p)); auto with arith. rewrite Nat.add_comm, Nat.sub_add; auto. apply pGivesDigit; auto. unfold Fnormalize in |- *; case (Z_zerop (Fnum p)); auto. simpl in |- *; auto with zarith. generalize H'; case p; unfold Fbounded, Fnormal, Fdigit in |- *; simpl in |- *. intros Fnum1 Fexp1 H'0 H'1. apply Z.le_trans with (m := (Fexp1 - Z.abs_nat (dExp b + Fexp1))%Z). rewrite inj_abs; auto with zarith. unfold Zminus in |- *; apply Zplus_le_compat_l; auto. apply Zle_Zopp; auto. apply inj_le; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz