Theorem: LoVe.linarith_example (LoVe/Lectures/LoVe06_InductivePredicates_Demo.lean)

State before:
i : ℤ
hi : i > 5
⊢ 2 * i + 3 > 11
Tactic:
linarith
State after:
no goals