simp only [pair', of_fraction, Fin.sum_univ_three, cons_val_zero, cons_val_one, head_cons,
  cons_val_two, tail_cons, Nat.cast_add]
d a b : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ pair' (of_fraction d a b) z = ↑a * z 2 + ↑b * (z 1 + z 2)
d a b : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ z 0 * ↑0 + z 1 * ↑b + z 2 * (↑a + ↑b) = ↑a * z 2 + ↑b * (z 1 + z 2)