proposition: Theorem Rcompare_half_r : forall x y, Rcompare x (y / 2) = Rcompare (2 * x) y.
proof: Proof. intros x y. rewrite <- (Rcompare_mult_r 2%R). unfold Rdiv. rewrite Rmult_assoc, Rinv_l, Rmult_1_r. now rewrite Rmult_comm. now apply IZR_neq. now apply IZR_lt. Qed.
imports: Coq(Psatz Reals ZArith) Zaux