simp only [h, and_self, ite_true]
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ ((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
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ (x - y) % y + y * ((x - y) / y + 1) = x