proposition: Lemma add_DN_correct : forall p x y, valid_lb x = true -> valid_lb y = true -> (valid_lb (add_DN p x y) = true /\ le_lower (toX (add_DN p x y)) (Xadd (toX x) (toX y))).
proof: Proof. intros p x y _ _; split; [reflexivity|]. unfold add_DN. rewrite add_slow_correct. unfold Xround, Xlift. set (z := Xadd _ _); case z; [exact I|]; intro zr. now apply Ropp_le_contravar, Generic_fmt.round_DN_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