proposition: Theorem Rcompare_half_l : forall x y, Rcompare (x / 2) y = Rcompare x (2 * 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