Theorem: Weight.one_le_E (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ 1 ≤ E w
Tactic:
simp only [E, le_add_iff_nonneg_left, zero_le']
State after:
no goals