proposition: Lemma inf_el_to_fun : ∀ (a : ℕ → ℝ) (P : ℕ → ℝ → Prop), (∀ N : ℕ, ∃ k : ℕ, (N ≤ k)%nat ∧ (P N (a k))) ⇒ ∃ f : ℕ → ℕ, ∀ l : ℕ, (l ≤ f l)%nat ∧ P l (a (f l)).
proof: Proof. Take a : (ℕ → ℝ). Take P : (ℕ → ℝ → Prop). apply choice with (R := fun (k : ℕ) (l : ℕ) ↦ ((k ≤ l)%nat ∧ P k (a l))). Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove