simp only [dom_iff, f_le_iff, f_apply, SetCoe.forall, Subtype.coe_mk, hE]
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hE : E w = E w'
h : w' ≤ w
⊢ w ≤ w'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hE : E w = E w'
h : w' ≤ w
⊢ ∀ x ∈ testvecs n d, E w' - pair w x ≤ E w' - pair w' x