proposition: Lemma one_IZR_r_R1 : forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.
proof: Proof. intros r n m [H1 H2] [H3 H4]; apply Zminus_eq, one_IZR_lt1. rewrite <-Z_R_minus; split. - replace (-1) with (r - (r + 1)) by (now rewrite Rminus_plus_distr, Rminus_diag, Rminus_0_l). unfold Rminus; apply Rplus_lt_le_compat; [assumption |]. now apply Ropp_le_contravar. - replace 1 with (r + 1 - r) by (now apply Rplus_minus_l). unfold Rminus; apply Rplus_le_lt_compat; try easy. now apply Ropp_lt_contravar. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField