{
  sorry
}
case a

⊢ ∀ (k : ℕ), 0 < k → (0 A k) = 0

case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0
case a

⊢ ∀ (n : ℕ), (∀ (k : ℕ), n < k → (n A k) = 0) → ∀ (k : ℕ), n + 1 < k → (n + 1 A k) = 0