simp only [h, ite_false, Nat.mul_zero, Nat.add_zero]
case base
x y : Nat
h : ¬(0 < y ∧ y ≤ x)
⊢ ((if 0 < y ∧ y ≤ x then (x - y) % y else x) + y * if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0) = x
no goals