Theorem: Int.pow_ge_zero (MLIR/Util/Arith.lean)

State before:
n : ℤ
m : ℕ
⊢ n ≥ 0 → n ^ m ≥ 0
Tactic:
revert n
State after:
m : ℕ
⊢ ∀ (n : ℤ), n ≥ 0 → n ^ m ≥ 0

State before:
m : ℕ
⊢ ∀ (n : ℤ), n ≥ 0 → n ^ m ≥ 0
Tactic:
induction m <;> intros n h <;> simp
State after:
case succ
n✝ : ℕ
n_ih✝ : ∀ (n : ℤ), n ≥ 0 → n ^ n✝ ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ Nat.succ n✝

State before:
acc : ℕ
ih : ∀ (n : ℤ), n ≥ 0 → n ^ acc ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ Nat.succ acc
Tactic:
case succ acc ih =>
  simp [pow_succ]; apply mul_ge_zero (ih _ h) h
State after:
no goals

State before:
acc : ℕ
ih : ∀ (n : ℤ), n ≥ 0 → n ^ acc ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ Nat.succ acc
Tactic:
simp [pow_succ]
State after:
acc : ℕ
ih : ∀ (n : ℤ), n ≥ 0 → n ^ acc ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ acc * n

State before:
acc : ℕ
ih : ∀ (n : ℤ), n ≥ 0 → n ^ acc ≥ 0
n : ℤ
h : n ≥ 0
⊢ 0 ≤ n ^ acc * n
Tactic:
apply mul_ge_zero (ih _ h) h
State after:
no goals