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

State before:
a b c d : Int
k : Nat
z : Int
h : z > 0
⊢ z ^ k > 0
Tactic:
induction k with
| zero    => simp [Int.pow_zero]
| succ k ih =>
  rw [Int.pow_succ]
  have h₂ := Int.mul_lt_mul_of_pos_left h ih
  simp at h₂
  exact h₂
State after:
no goals

State before:
case zero
a b c d z : Int
h : z > 0
⊢ z ^ 0 > 0
Tactic:
simp [Int.pow_zero]
State after:
no goals

State before:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
⊢ z ^ (k + 1) > 0
Tactic:
rw [Int.pow_succ]
State after:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
⊢ z ^ k * z > 0

State before:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
⊢ z ^ k * z > 0
Tactic:
have h₂ := Int.mul_lt_mul_of_pos_left h ih
State after:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : z ^ k * 0 < z ^ k * z
⊢ z ^ k * z > 0

State before:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : z ^ k * 0 < z ^ k * z
⊢ z ^ k * z > 0
Tactic:
simp at h₂
State after:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : 0 < z ^ k * z
⊢ z ^ k * z > 0

State before:
case succ
a b c d z : Int
h : z > 0
k : Nat
ih : z ^ k > 0
h₂ : 0 < z ^ k * z
⊢ z ^ k * z > 0
Tactic:
exact h₂
State after:
no goals