cases this
m n : Nat
x₁ x₂ : Fin m
y₁ y₂ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₂
this : y₁ = y₂
⊢ x₁ = x₂ ∧ y₁ = y₂
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
⊢ x₁ = x₂ ∧ y₁ = y₁