rw [ha, hb, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add]
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
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑a * v i 2 + ↑b * (v i 1 + v i 2)
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
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2)
⊢ ↑a' * v i 2 + ↑b' * (v i 1 + v i 2) ≤ ↑m * (↑a' * v i 2 + ↑b' * (v i 1 + v i 2))