no goals
f : Nat → Bool
n✝ n : Nat
⊢ (all f n && allTR.loop f (0 + n) 0) = all f (0 + n)
simp [allTR.loop]
f : Nat → Bool
n✝ m n : Nat
⊢ (all f n && f n && allTR.loop f (succ (m + n)) m) = all f (succ (m + n))
f : Nat → Bool
n✝ m n : Nat
⊢ (all f n && allTR.loop f (succ m + n) (succ m)) = all f (succ m + n)
rw [allTR.loop, add_sub_self_left, ← Bool.and_assoc, succ_add]
no goals
f : Nat → Bool
n✝ m n : Nat
⊢ (all f n && f n && allTR.loop f (succ (m + n)) m) = all f (succ (m + n))
exact go m (succ n)