proposition: Lemma valid_lb_real : forall b, F.toX b = Xreal (proj_val (F.toX b)) -> F.valid_lb b = true.
proof: Proof. now intros b Hb; rewrite F'.valid_lb_real; [|rewrite F.real_correct, Hb]. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval