proposition: Lemma le_INR : forall n m:nat, (n <= m)%nat -> INR n <= INR m.
proof: Proof. intros n m [I | ->]%Nat.le_lteq. - now left; apply lt_INR. - now right. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField