Theorem: one_le_d_minus_one (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≤ d - 1
Tactic:
have h := two_le_d d
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
h : 2 ≤ d
⊢ 1 ≤ d - 1

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
h : 2 ≤ d
⊢ 1 ≤ d - 1
Tactic:
omega
State after:
no goals