α : Type ?u.305323
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
⊢ C = 0 ∨ 0 < C ∧ 0 ≤ r
α : Type ?u.305323
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
⊢ C = 0 ∨ 0 < C ∧ 0 ≤ r
have : 0 ≤ C := by simpa only [pow_zero, mul_one] using h 0
α : Type ?u.305323
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
hC : 0 < C
⊢ 0 ≤ r
α : Type ?u.305323
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
⊢ C = 0 ∨ 0 < C ∧ 0 ≤ r
refine' this.eq_or_lt.elim (fun h => Or.inl h.symm) fun hC => Or.inr ⟨hC, _⟩
α : Type ?u.305323
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
hC : 0 < C
⊢ 0 ≤ C * r
α : Type ?u.305323
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
hC : 0 < C
⊢ 0 ≤ r
refine' nonneg_of_mul_nonneg_right _ hC
no goals
α : Type ?u.305323
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
this : 0 ≤ C
hC : 0 < C
⊢ 0 ≤ C * r
simpa only [pow_one] using h 1
no goals
α : Type ?u.305323
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedSemiring R
C r : R
h : ∀ (n : ℕ), 0 ≤ C * r ^ n
⊢ 0 ≤ C
simpa only [pow_zero, mul_one] using h 0