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

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
⊢ w ≤ w' ↔ ∀ (j : Fin (Nat.succ n)), w j ≤ w' j
Tactic:
rfl
State after:
no goals