proposition: Lemma single_z_r_R1_depr : forall r (n m:Z), r < IZR n -> IZR n <= r + 1 -> r < IZR m -> IZR m <= r + 1 -> n = m.
proof: Proof. now intros r n m Hlt Hle Hlt' Hle'; apply (one_IZR_r_R1 r). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField