proposition: Theorem Rcompare_middle : forall x d u, Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2).
proof: Proof. intros x d u. rewrite <- (Rcompare_plus_r (- x / 2 - d / 2) x). rewrite <- (Rcompare_mult_r (/2) (x - d)). field_simplify (x + (- x / 2 - d / 2))%R. now field_simplify ((d + u) / 2 + (- x / 2 - d / 2))%R. apply Rinv_0_lt_compat. now apply IZR_lt. Qed.
imports: Coq(Psatz Reals ZArith) Zaux