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