proposition: Lemma archimed_mod : ∀ x : ℝ, ∃ n : ℕ, INR(n) > x.
proof: Proof. Take x : ℝ. Either (x <= 0) or (0 < x). - Case (x <= 0). Choose n := 1%nat. We claim that (INR 1 > INR 0). { We need to show that ( 1 > 0 ). We conclude that (1 > 0). } It holds that (x <= INR 0). We conclude that (n > x). - Case (0 < x). By archimed it holds that (IZR( up x) > x ∧ IZR( up x ) - x ≤ 1). It holds that (IZR( up x ) > x). It holds that (0 < IZR( up x )). By lt_0_IZR it holds that (0 < up x)%Z. It holds that (0 <= up x)%Z. By IZN it holds that (∃ k : ℕ, up x = Z.of_nat k). Obtain such a k. It holds that (up x = Z.of_nat k) (ii). Choose n := k. We need to show that (INR k > x). By INR_IZR_INZ it holds that (INR k = IZR (Z.of_nat k)). We claim that (IZR (up x) = IZR (Z.of_nat k)). { rewrite (ii). reflexivity. } We need to show that (x < k). We conclude that (& x < up x = Z.of_nat k = k). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations