proposition: Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.
proof: Proof. intros n m H; apply Rnot_lt_ge; intros H2%lt_IZR. now apply (Zle_not_lt n m). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField