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, midpoint, sm1. rewrite !real_correct. rewrite (scale2_correct _ _ He). rewrite add_exact_correct. do 2 (case toX; [easy|]). unfold StoZ. rewrite ZtoE_correct. change (bpow radix2 (-1)) with (/2)%R. clear x y; simpl; intros x y _ _ Hxy. now split; [|lra]. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig