proposition: Lemma sqr_UP_correct : forall prec x, F.valid_lb x = true \/ F.valid_ub x = true -> F.valid_ub (F.mul_UP prec x x) = true /\ le_upper (F.toX x * F.toX x)%XR (F.toX (F.mul_UP prec x x)).
proof: Proof. intros prec x Vx. apply F.mul_UP_correct. unfold F.is_non_neg', F.is_non_pos', F.is_non_pos_real, F.is_non_neg_real. destruct F.toX as [|xr]. intuition. destruct (Rlt_or_le 0 xr) as [H|H]. apply Rlt_le in H. now left. now right ; left. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic