Theorem: partial_geometric_bound (Ray/Misc/Bounds.lean)

State before:
a : ℝ
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
⊢ ∀ n ∉ N, 0 ≤ a ^ n
Tactic:
intro n _
State after:
a : ℝ
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
n : ℕ
a✝ : n ∉ N
⊢ 0 ≤ a ^ n

State before:
a : ℝ
N : Finset ℕ
a0 : 0 ≤ a
a1 : a < 1
n : ℕ
a✝ : n ∉ N
⊢ 0 ≤ a ^ n
Tactic:
bound
State after:
no goals