proposition: Theorem Rcompare_mult_r : forall z x y, (0 < z)%R -> Rcompare (x * z) (y * z) = Rcompare x y.
proof: Proof. intros z x y Hz. destruct (Rcompare_spec x y) as [H|H|H]. apply Rcompare_Lt. now apply Rmult_lt_compat_r. apply Rcompare_Eq. now rewrite H. apply Rcompare_Gt. now apply Rmult_lt_compat_r. Qed.
imports: Coq(Psatz Reals ZArith) Zaux