proposition: Lemma midpoint_correct : forall x y, sensible_format = true -> real x = true -> real y = true -> (toR x <= toR y)%R -> real (midpoint x y) = true /\ (toR x <= toR (midpoint x y) <= toR y)%R.
proof: Proof. intros x y He. unfold toR, FtoX, midpoint. rewrite !real_correct. rewrite (Fscale2_correct _ _ _ He). rewrite Fadd_exact_correct. unfold toX. do 2 (case FtoX; [easy|]). change (bpow radix2 (ZtoS (-1))) with (/2)%R. clear x y; simpl; intros x y _ _ Hxy. now split; [|lra]. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig