proposition: Theorem FnormalizeCorrect : forall p : float, Fnormalize p = p :>R.
proof: Proof. intros p; unfold Fnormalize in |- *. case (Z_zerop (Fnum p)). case p; intros Fnum1 Fexp1 H'; unfold FtoRradix, FtoR in |- *; rewrite H'; simpl in |- *; auto with real. apply trans_eq with 0%R; auto with real. intros H'; unfold FtoRradix in |- *; apply FshiftCorrect; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz