proposition: Lemma valid_ub_neg x : F.valid_ub (F.neg x) = F.valid_lb x.
proof: Proof. generalize (F.real_correct x). generalize (F.real_correct (F.neg x)). generalize (F.neg_correct x). rewrite !F.classify_correct, !F.valid_lb_correct, !F.valid_ub_correct. case F.classify; intro Hx; rewrite Hx; [|now case F.toX, F.toX..]. now case F.toX; [easy|]; intros rx; simpl; case F.classify. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic