proposition: Lemma valid_ub_zero : F.valid_ub F.zero = true.
proof: Proof. generalize (F.valid_ub_correct F.zero). generalize (F.classify_correct F.zero). rewrite F.real_correct, F.zero_correct. now case F.classify. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic