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