proposition: Theorem FnormalFabs : forall p : float, Fnormal p -> Fnormal (Fabs p).
proof: Proof. intros p; case p; intros a e H; split. simpl in |- *; case H; intros H1 H2; simpl in |- *; auto. now apply absFBounded. simpl; rewrite <- (Z.abs_eq radix); auto with zarith. rewrite <- Zabs_Zmult. rewrite (fun x => Z.abs_eq (Z.abs x)); auto with zarith. apply H. Qed.
imports: Reals ZArith List PeanoNat Psatz