proposition: Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat.
proof: Proof. intros n m [I | E]. - now apply Nat.lt_le_incl, INR_lt. - now apply Nat.eq_le_incl, INR_eq. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField