proposition: Theorem F2R_minus : forall f1 f2 : float beta, F2R (Fminus f1 f2) = (F2R f1 - F2R f2)%R.
proof: Proof. intros f1 f2; unfold Fminus. rewrite F2R_plus, F2R_opp. ring. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop