Theorem: chapter03.factor_in_descFactorial (FormalBook/Chapter_03.lean)

State before:
n k p l : ℕ
h_klen : k ≤ n
h_klp : k < p
hp : p.Prime
h_pow_div : p ^ l ∣ n.descFactorial k
h_1lel : 1 ≤ l
⊢ ∃ i ≤ k - 1, p ^ l ∣ n - i
Tactic:
sorry
State after:
no goals