proposition: Theorem FnormalFop : forall p : float, Fnormal p -> Fnormal (Fopp p).
proof: Proof. intros p H; split. apply oppBounded; apply H. replace (Z.abs (radix * Fnum (Fopp p))) with (Z.abs (radix * Fnum p)); try apply H. destruct p. simpl. now rewrite Z.mul_opp_r, Z.abs_opp. Qed.
imports: Reals ZArith List PeanoNat Psatz