proposition: Theorem Fopp_correct : forall x : float, Fopp x = (- x)%R :>R.
proof: Proof. unfold FtoRradix, FtoR, Fopp in |- *; simpl in |- *. intros x. rewrite Ropp_Ropp_IZR; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz