apply dom_of_pair_le
case intro.intro
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ of_fraction d a' b' ≤ of_fraction d a b
case intro.intro.h
d : ℕ
inst✝ : NeZero d
a b a' b' : ℕ
hab : a ≠ 0 ∨ b ≠ 0
hc : Nat.Coprime a' b'
h : a' * b = b' * a
m : ℕ
ha : a = m * a'
hb : b = m * b'
hmz : m ≠ 0
hm : 1 ≤ ↑m
⊢ ∀ (a_1 : ↑(testvecs 2 d)),
    0 ≤ pair' (of_fraction d a' b') (v a_1) → pair' (of_fraction d a' b') (v a_1) ≤ pair' (of_fraction d a b) (v a_1)