English
Let p be prime. If p^k ∣ a, p^l ∣ b, and p^{k+l+1} ∣ a b, then p^{k+1} ∣ a or p^{l+1} ∣ b.
Русский
Пусть p простое. Если p^k делит a, p^l делит b, и p^{k+l+1} делит ab, то p^{k+1} делит a или p^{l+1} делит b.
LaTeX
$$$\\forall k,l:\\, \\mathbb{N},\\; \\bigl(p^k \\mid a\\bigr) \\land \\bigl(p^l \\mid b\\bigr) \\land \\bigl(p^{k+l+1} \\mid a b\\bigr) \\Rightarrow p^{k+1} \\mid a \\lor p^{l+1} \\mid b.$$$
Lean4
theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul (hp : Prime p) {a b : M} {k l : ℕ} :
p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b :=
fun ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩ =>
have h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z) := by
simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz
have hp0 : p ^ (k + l) ≠ 0 := pow_ne_zero _ hp.ne_zero
have hpd : p ∣ x * y := ⟨z, by rwa [mul_right_inj' hp0] at h⟩
(hp.dvd_or_dvd hpd).elim (fun ⟨d, hd⟩ => Or.inl ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
fun ⟨d, hd⟩ => Or.inr ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩
