no goals
f : Nat → Bool
n✝ n : Nat
⊢ (any f n || anyTR.loop f (0 + n) 0) = any f (0 + n)
simp [anyTR.loop]
f : Nat → Bool
n✝ m n : Nat
⊢ (any f n || f n || anyTR.loop f (succ (m + n)) m) = any f (succ (m + n))
f : Nat → Bool
n✝ m n : Nat
⊢ (any f n || anyTR.loop f (succ m + n) (succ m)) = any f (succ m + n)
rw [anyTR.loop, add_sub_self_left, ← Bool.or_assoc, succ_add]
no goals
f : Nat → Bool
n✝ m n : Nat
⊢ (any f n || f n || anyTR.loop f (succ (m + n)) m) = any f (succ (m + n))
exact go m (succ n)