proposition: Lemma rnd_binop_UP_correct op Rop : (forall mode p x y, toX (op mode p x y) = Xround radix mode (prec p) (Xlift2 Rop (toX x) (toX y))) -> forall p x y, le_upper (Xlift2 Rop (toX x) (toX y)) (toX (op rnd_UP p x y)).
proof: Proof. intros H p x y; rewrite H; clear H. set (z := Xlift2 _ _ _). unfold Xround, Xlift. case z; [exact I|intro z'; simpl]. now apply Generic_fmt.round_UP_pt, FLX.FLX_exp_valid. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig