Enumerate a small natural

2/4 ~10 minlean

Use Presburger arithmetic to enumerate naturals below three.

4 lines · Lean 4

import Mathlib

example (n : Nat) (h : n < 3) : n = 0 ∨ n = 1 ∨ n = 2 := by
  sorry

Objectifs

Indices

Voir la solution

import Mathlib

example (n : Nat) (h : n < 3) : n = 0 ∨ n = 1 ∨ n = 2 := by
  omega