proposition: Theorem Fminus_correct : forall x y : float, Fminus x y = (x - y)%R :>R.
proof: Proof. intros x y; unfold Fminus in |- *. rewrite Fplus_correct. rewrite Fopp_correct; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz