destruct_dropn — Mathlib

English

destruct(drop s n) = destruct s bind drop.aux n.

Русский

destruct(drop(s,n)) = destruct(s)bind drop.aux(n).

LaTeX

$$$$\operatorname{destruct}(\operatorname{drop}(s,n)) = \operatorname{destruct}(s) \bind \operatorname{drop.aux}(n).$$$$

Lean4

theorem destruct_dropn : ∀ (s : WSeq α) (n), destruct (drop s n) = destruct s >>= drop.aux n
  | _, 0 => (bind_pure' _).symm
  | s, n + 1 => by
    rw [← dropn_tail, destruct_dropn _ n, destruct_tail, LawfulMonad.bind_assoc]
    rfl

Похожие утверждения