proposition: Theorem Rcompare_IZR : forall x y, Rcompare (IZR x) (IZR y) = Z.compare x y.
proof: Proof. intros x y. case Rcompare_spec ; intros H ; apply sym_eq. apply Zcompare_Lt. now apply lt_IZR. apply Zcompare_Eq. now apply eq_IZR. apply Zcompare_Gt. now apply lt_IZR. Qed.
imports: Coq(Psatz Reals ZArith) Zaux