Properties of the order on a binary product of Fin types

theorem Fin.prod_zero_zero_lt_iff {p q : ℕ} (i : Fin (p + 1) × Fin (q + 1)) : (0, 0) < i ↔ 0 < ↑i.1 + ↑i.2

theorem Fin.prod_lt_last_last_iff {p q : ℕ} (i : Fin (p + 1) × Fin (q + 1)) : i < (last p, last q) ↔ ↑i.1 + ↑i.2 < p + q

theorem Fin.prod_exists_lt_lt_of_le_of_le {p q : ℕ} (k₀ k₂ : Fin p × Fin q) (h₀₂ : k₀ ≤ k₂) (h : ↑k₀.1 + ↑k₀.2 + 2 ≤ ↑k₂.1 + ↑k₂.2) : ∃ (k₁ : Fin p × Fin q), k₀ < k₁ ∧ k₁ < k₂