CovBy.coe_fin

theorem CovBy.coe_fin : ∀ {n : ℕ} {a b : Fin n}, a ⋖ b → ↑a ⋖ ↑b

This theorem, `CovBy.coe_fin`, states that for any given natural number `n` and any two elements `a` and `b` of the finite ordinal type `Fin n`, if `a` is covered by `b` (denoted as `a ⋖ b`), then the natural number representation of `a` (obtained by the coercion `↑a`) is also covered by the natural number representation of `b` (`↑b`). The theorem is an alias for the reverse direction of `Fin.coe_covBy_iff`.

More concisely: For any natural numbers `n`, `m` and finite ordinal elements `a` and `b` of `Fin n`, if `a ⋖ b` then `↑a ≤ ↑b`.