proposition: Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z.
proof: Proof. unfold Rle; intros n m [H%lt_IZR | ->%eq_IZR]. - now apply Z.lt_le_incl. - now apply Z.le_refl. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField