proposition: Lemma sub_DN_correct : forall p x y, valid_lb x = true -> valid_ub y = true -> (valid_lb (sub_DN p x y) = true /\ le_lower (toX (sub_DN p x y)) (Xsub (toX x) (toX y))).
proof: Proof. intros p x y _ _; split; [easy|]. now apply (rnd_binop_DN_correct _ _ (@Fsub_correct _)). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig