proposition: Theorem FsubnormFopp : forall p : float, Fsubnormal p -> Fsubnormal (Fopp p).
proof: Proof. intros p H'; repeat split; simpl in |- *; auto with zarith; try apply H'. rewrite Zabs_Zopp; apply H'. rewrite <- Zopp_mult_distr_r; rewrite Zabs_Zopp; apply H'. Qed.
imports: Reals ZArith List PeanoNat Psatz