Exhibit a natural number equal to `n + n`.
2 lines · Lean 4
Objectifs
- Exhibit a natural number equal to `n + n`.
Indices
Voir la solution
theorem double_exists (n : Nat) : ∃ m, m = n + n := by exact ⟨n + n, rfl⟩
Exhibit a natural number equal to `n + n`.
theorem double_exists (n : Nat) : ∃ m, m = n + n := by exact ⟨n + n, rfl⟩