proposition: Theorem Rcompare_floor_ceil_middle : forall x, IZR (Zfloor x) <> x -> Rcompare (x - IZR (Zfloor x)) (/ 2) = Rcompare (x - IZR (Zfloor x)) (IZR (Zceil x) - x).
proof: Proof. intros x Hx. rewrite Zceil_floor_neq with (1 := Hx). rewrite plus_IZR. destruct (Rcompare_spec (x - IZR (Zfloor x)) (/ 2)) as [H1|H1|H1] ; apply sym_eq. apply Rcompare_Lt. apply Rplus_lt_reg_l with (x - IZR (Zfloor x))%R. replace (x - IZR (Zfloor x) + (x - IZR (Zfloor x)))%R with ((x - IZR (Zfloor x)) * 2)%R by ring. replace (x - IZR (Zfloor x) + (IZR (Zfloor x) + 1 - x))%R with (/2 * 2)%R by field. apply Rmult_lt_compat_r with (2 := H1). now apply IZR_lt. apply Rcompare_Eq. replace (IZR (Zfloor x) + 1 - x)%R with (1 - (x - IZR (Zfloor x)))%R by ring. rewrite H1. field. apply Rcompare_Gt. apply Rplus_lt_reg_l with (x - IZR (Zfloor x))%R. replace (x - IZR (Zfloor x) + (x - IZR (Zfloor x)))%R with ((x - IZR (Zfloor x)) * 2)%R by ring. replace (x - IZR (Zfloor x) + (IZR (Zfloor x) + 1 - x))%R with (/2 * 2)%R by field. apply Rmult_lt_compat_r with (2 := H1). now apply IZR_lt. Qed.
imports: Coq(Psatz Reals ZArith) Zaux