x y : Nat
⊢ Nat.div x y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0
x y : Nat
⊢ x / y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0
show Nat.div x y = _
x y : Nat
⊢ ite (0 < y ∧ y ≤ x) (Nat.div (x - y) y + 1) 0 = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0
x y : Nat
⊢ Nat.div x y = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0
rw [Nat.div]
no goals
x y : Nat
⊢ ite (0 < y ∧ y ≤ x) (Nat.div (x - y) y + 1) 0 = ite (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0
rfl