proposition: Lemma mul_UP_correct : forall p x y, ((is_non_neg' x /\ is_non_neg' y) \/ (is_non_pos' x /\ is_non_pos' y) \/ (is_non_pos_real x /\ is_non_neg_real y) \/ (is_non_neg_real x /\ is_non_pos_real y)) -> valid_ub (mul_UP p x y) = true /\ le_upper (Xmul (toX x) (toX y)) (toX (mul_UP p x y)).
proof: Proof. intros p x y _; split; [reflexivity|]. unfold mul_UP. rewrite mul_correct. unfold Xround, Xlift. set (z := Xmul _ _); case z; [exact I|]; intro zr. now apply Generic_fmt.round_UP_pt, FLX.FLX_exp_valid. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig