n power : Nat
h₁ : power > 0
h₂ : power < n
this : power * 2 = power + power
⊢ n - power * 2 < n - power
n power : Nat
h₁ : power > 0
h₂ : power < n
⊢ n - power * 2 < n - power
have : power * 2 = power + power := by simp_arith
n power : Nat
h₁ : power > 0
h₂ : power < n
this : power * 2 = power + power
⊢ n - power - power < n - power
n power : Nat
h₁ : power > 0
h₂ : power < n
this : power * 2 = power + power
⊢ n - power * 2 < n - power
rw [this, Nat.sub_add_eq]
no goals
n power : Nat
h₁ : power > 0
h₂ : power < n
this : power * 2 = power + power
⊢ n - power - power < n - power
exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁
no goals
n power : Nat
h₁ : power > 0
h₂ : power < n
⊢ power * 2 = power + power
simp_arith