get the lastDrop

Stream: Is there code for X?

[Moritz Firsching]

I'm trying to get the following version of Legendre's theorem:
$(p - 1)v_p(n!)=\frac{n-s_p(n)}{p-1}$
where $v_p$ is the $p$-adic valuation and $s_p(n)$ is the sum of the digits of $n$ in base $p$
We have a version of this, which is docs4#Nat.Prime.multiplicity_factorial, but this is a little different.
So far I can prove:

theorem ofDigits_div_pow_eq_sum_drop (b i : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b)
    (w₂ : ∀ h : L ≠ [], L.getLast h ≠ 0) :
 ((ofDigits b L) / b ^ i) = ∑ j : Fin (L.drop i).length, ((L.drop i).get j) * b ^ j  := by
  sorry -- proof to long for the margin in zulip

but I'm not sure this is the best way to do it.

On the way I needed the following three statements about lists, which I couldn't find:

theorem non_empty_of_drop_non_empty.{u} {α : Type u} {as : List α} {i : ℕ}
    (h: as.drop i ≠ []) : as ≠ []  := by
  have : ∃ a, a ∈ as.drop i := by exact List.exists_mem_of_ne_nil (List.drop i as) h
  obtain ⟨a, ha⟩ := this
  refine' List.ne_nil_of_mem <| List.mem_of_mem_drop ha

theorem lt_of_drop_ne_nil.{u} {α : Type u} {as : List α} {i : ℕ} (h : List.drop i as ≠ []) :
    i < List.length as :=
  Decidable.byContradiction fun hi => h <| (List.drop_eq_nil_of_le <| not_lt.mp hi)

theorem getLast_drop.{u} {α : Type u} {as : List α} {i : ℕ} (h : as.drop i ≠ []) :
    (List.getLast as <| non_empty_of_drop_non_empty h) = (as.drop i).getLast h := by
  simp only [List.getLast_eq_get]
  have h' : i + (as.length - i - 1) = as.length - 1 := by
    rw [Nat.sub_right_comm, ← Nat.add_sub_assoc (le_pred_of_lt <| lt_of_drop_ne_nil h) i]
    exact add_sub_self_left i (List.length as - 1)
  have h'' : i + (as.length - i - 1) < as.length :=
      h' ▸ sub_lt (Iff.mpr List.length_pos <| non_empty_of_drop_non_empty h) Nat.one_pos
  simpa [h'] using List.get_drop as h''

Should any of those three become part of Std?

[Scott Morrison]

I like the first two, and they should put in mathlib4 or std4. For the third one, I would probably generalize the non_empty_of_drop_non_empty h to an arbitrary w. This lemma also seems more natural if the equality is flipped over.

[Moritz Firsching]

For the first one, I noticed for completeness there is also the take version and the contraposed version.
There is docs4#Data.List.take_eq_nil_iff, which is only in mathlib, not in std (but there is no corresponding drop_eq_nil_iff.
So I made std4#179 for the first.