Theorem: verus_lemma_mul_induction (VerusLeanStd/MulInternals.lean)

State before:
f : ℤ → Bool
h1 : f 0 = true
h2 : ∀ (i : ℤ), i ≥ 0 ∧ f i = true → f (i + 1) = true
h3 : ∀ (i : ℤ), i ≤ 0 ∧ f i = true → f (i - 1) = true
⊢ ∀ (i : ℤ), f i = true
Tactic:
sorry
State after:
no goals