proposition: Lemma valid_lb_real f : F.real f = true -> F.valid_lb f = true.
proof: Proof. generalize (F.valid_lb_correct f). generalize (F.classify_correct f). now case F.classify; try easy; intro H; rewrite H. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic