proposition: Lemma mul_UP_correct : forall p x y, ((F.is_non_neg x /\ F.is_non_neg y) \/ (F.is_non_pos x /\ F.is_non_pos y) \/ (F.is_non_pos_real x /\ F.is_non_neg_real y) \/ (F.is_non_neg_real x /\ F.is_non_pos_real y)) -> (F.valid_ub (F.mul_UP p x y) = true /\ le_upper (Xmul (F.toX x) (F.toX y)) (F.toX (F.mul_UP p x y))).
proof: Proof. intros prec x y H. apply F.mul_UP_correct. destruct H as [[[H1 H2] [H3 H4]]|[[[H1 H2] [H3 H4]]|[[H1 H2]|[H1 H2]]]]. - left ; unfold F.is_non_neg' ; split. now destruct (F.toX x). now destruct (F.toX y). - right ; left ; unfold F.is_non_pos' ; split. now destruct (F.toX x). now destruct (F.toX y). - intuition. - intuition. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic