Theorem: Fin.pair_ge_left (LeanColls/MathlibUpstream.lean)

State before:
m n : ℕ
x : Fin m
y : Fin n
⊢ ↑(x.pair y) ≥ ↑x * n
Tactic:
simp [pair]
State after:
no goals