proposition: Theorem FNevenFop : forall p : float, FNeven p -> FNeven (Fopp p).
proof: Proof. intros p; unfold FNeven in |- *. rewrite Fnormalize_Fopp; auto with zarith arith. intros; apply FevenFop; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz