Theorem: List.length_rtake (LeanCamCombi/Mathlib/Data/List/DropRight.lean)

State before:
α : Type u_1
l✝ l' l₀ l₁ l₂ : List α
a b : α
m n✝ n : ℕ
l : List α
⊢ l.length - (l.length - n) = min n l.length
Tactic:
rw [Nat.sub_sub_eq_min, min_comm]
State after:
no goals