-- Let's explore dot patterns



data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ -> ℕ -> ℕ
zero + m = m
succ n + m = succ (n + m)

data Even : ℕ -> Set where
  base-case : Even zero
  ind-step : ∀ (n : ℕ) -> Even n -> Even (succ (succ n))

theorem-add-even : ∀ (n m : ℕ) -> Even n -> Even m -> Even (n + m)
theorem-add-even .zero m base-case hyp2 = hyp2
theorem-add-even .(succ (succ n')) m (ind-step n' hyp1') hyp2 = ind-step (n' + m) (theorem-add-even n' m hyp1' hyp2)

-- C-c C-a to "automatically" fill in a goal. Caution: this does not always succeed!
-- It can also sometimes give the wrong answer.