calc
  _ = 0 * pair' (of_fraction d I.a₁ I.b₁) (v i) + 1 * pair' (of_fraction d I.a₂ I.b₂) (v i) := by
      rw [one_mul, zero_mul, zero_add]
  _ ≤ k₁ * pair' (of_fraction d I.a₁ I.b₁) (v i) + k₂ * pair' (of_fraction d I.a₂ I.b₂) (v i) :=
      add_le_add (Int.mul_le_mul_of_nonneg_right (by exact_mod_cast hk₁.le) hi')
                 (Int.mul_le_mul_of_nonneg_right (by exact_mod_cast hk₂) hi)
  _ = _ := by
      rw [h₁, h₂, pair'_of_fraction_add, Pi.add_apply, pair'_of_fraction_mul,
          pair'_of_fraction_mul]
case intro.intro.intro.intro.intro.h
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ pair' (of_fraction d I.a₂ I.b₂) (v i) ≤ pair' (of_fraction d a b) (v i)
no goals