proposition: Theorem Rcompare_plus_r : forall z x y, Rcompare (x + z) (y + z) = Rcompare x y.
proof: Proof. intros z x y. destruct (Rcompare_spec x y) as [H|H|H]. apply Rcompare_Lt. now apply Rplus_lt_compat_r. apply Rcompare_Eq. now rewrite H. apply Rcompare_Gt. now apply Rplus_lt_compat_r. Qed.
imports: Coq(Psatz Reals ZArith) Zaux