proposition: Lemma sub_UP_correct : forall p x y, valid_ub x = true -> valid_lb y = true -> (valid_ub (sub_UP p x y) = true /\ le_upper (Xsub (toX x) (toX y)) (toX (sub_UP p x y))).
proof: Proof. intros p x y _ _; split; [reflexivity|]. unfold sub_UP. rewrite Xsub_split. assert (H : toX (neg y) = Xneg (toX y)); [|rewrite <-H; clear H]. { now generalize (neg_correct y); case y. } now apply add_UP_correct. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig