no goals
x y : Nat
⊢ Nat.modCore x y = x % y
cases x with
| zero =>
  rw [Nat.modCore]
  exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
| succ x => rfl
case zero
y : Nat
⊢ ite (0 < y ∧ y ≤ zero) (Nat.modCore (zero - y) y) zero = zero % y
case zero
y : Nat
⊢ Nat.modCore zero y = zero % y
rw [Nat.modCore]
no goals
case zero
y : Nat
⊢ ite (0 < y ∧ y ≤ zero) (Nat.modCore (zero - y) y) zero = zero % y
exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
no goals
case succ
y x : Nat
⊢ Nat.modCore (succ x) y = succ x % y
rfl