proposition: Lemma div_DN_correct : forall p x y, ((is_real_ub x /\ is_neg_real y) \/ (is_real_lb x /\ is_pos_real y)) -> valid_lb (div_DN p x y) = true /\ le_lower (toX (div_DN p x y)) (Xdiv (toX x) (toX y)).
proof: Proof. intros p x y _; split; [easy|]. unfold div_DN. rewrite (@Fdiv_correct radix). set (z := Xdiv _ _). unfold Xround, Xlift. case z; [exact I|intro z']. unfold le_lower, Xneg; simpl; apply Ropp_le_contravar. now apply Generic_fmt.round_DN_pt, FLX.FLX_exp_valid. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig