English
Let p be prime and m, n ∈ ℤ, with k, l ∈ ℕ, such that p^k | m, p^l | n, and p^{k+l+1} | mn. Then p^{k+1} | m or p^{l+1} | n.
Русский
Пусть p — простое число, m, n ∈ ℤ, и k, l ∈ ℕ таковы, что p^k | m, p^l | n и p^{k+l+1} | mn. Тогда p^{k+1} | m или p^{l+1} | n.
LaTeX
$$$\forall p \in \mathbb{N}, \mathrm{Prime}(p) \to \forall m,n \in \mathbb{Z}, \forall k,l \in \mathbb{N}, p^{k} \mid m \to p^{l} \mid n \to p^{(k+l+1)} \mid m n \to p^{k+1} \mid m \lor p^{l+1} \mid n.$$$
Lean4
theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : Nat.Prime p) {m n : ℤ} {k l : ℕ}
(hpm : ↑(p ^ k) ∣ m) (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k + l + 1)) ∣ m * n) :
↑(p ^ (k + 1)) ∣ m ∨ ↑(p ^ (l + 1)) ∣ n :=
have hpm' : p ^ k ∣ m.natAbs := Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpm
have hpn' : p ^ l ∣ n.natAbs := Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpn
have hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs := by rw [← Int.natAbs_mul];
apply Int.natCast_dvd_natCast.1 <| Int.dvd_natAbs.2 hpmn
let hsd := Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd.elim (fun hsd1 => Or.inl (by apply Int.dvd_natAbs.1; apply Int.natCast_dvd_natCast.2 hsd1)) fun hsd2 =>
Or.inr (by apply Int.dvd_natAbs.1; apply Int.natCast_dvd_natCast.2 hsd2)
