Theorem: Weight.E_w1 (Weights/Degree1.lean)

State before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ E (w1 n) = 1
Tactic:
rw [E, sum_w1]
State after:
n✝ n : ℕ
inst✝ : NeZero n
⊢ n * 1 / (n + 1) + 1 = 1

State before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ n * 1 / (n + 1) + 1 = 1
Tactic:
simp [Nat.div_eq_zero_iff]
State after:
no goals