Theorem: Smt.Reconstruct.Int.non_zero_even_pow (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
⊢ z ^ k > 0
Tactic:
match Int.lt_trichotomy z 0 with
| Or.inl hneg => exact pow_neg_even hneg h₂
| Or.inr (Or.inl hzero) => rw [hzero] at h₁; simp at h₁
| Or.inr (Or.inr hpos)  => exact pow_pos hpos
State after:
no goals

State before:
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
hneg : z < 0
⊢ z ^ k > 0
Tactic:
exact pow_neg_even hneg h₂
State after:
no goals

State before:
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
hzero : z = 0
⊢ z ^ k > 0
Tactic:
rw [hzero] at h₁
State after:
a b c d : Int
k : Nat
z : Int
h₁ : 0 ≠ 0
h₂ : k % 2 = 0
hzero : z = 0
⊢ z ^ k > 0

State before:
a b c d : Int
k : Nat
z : Int
h₁ : 0 ≠ 0
h₂ : k % 2 = 0
hzero : z = 0
⊢ z ^ k > 0
Tactic:
simp at h₁
State after:
no goals

State before:
a b c d : Int
k : Nat
z : Int
h₁ : z ≠ 0
h₂ : k % 2 = 0
hpos : 0 < z
⊢ z ^ k > 0
Tactic:
exact pow_pos hpos
State after:
no goals