English
If y_n(a)^2 divides y_t(a) then y_n(a) divides t.
Русский
Если y_n(a)^2 делит y_t(a), тогда y_n(a) делит t.
LaTeX
$$$y^{(a)}_{n}{}^{2} \\mid y^{(a)}_{t} \\Rightarrow y^{(a)}_{n} \\mid t$$$
Lean4
theorem dvd_of_ysq_dvd {n t} (h : yn a1 n * yn a1 n ∣ yn a1 t) : yn a1 n ∣ t :=
have nt : n ∣ t := (y_dvd_iff a1 n t).1 <| dvd_of_mul_left_dvd h
n.eq_zero_or_pos.elim (fun n0 => by rwa [n0] at nt ⊢) fun n0l : 0 < n =>
by
let ⟨k, ke⟩ := nt
have : yn a1 n ∣ k * xn a1 n ^ (k - 1) :=
Nat.dvd_of_mul_dvd_mul_right (strictMono_y a1 n0l) <|
modEq_zero_iff_dvd.1 <| by
have xm := (xy_modEq_yn a1 n k).right; rw [← ke] at xm
exact (xm.of_dvd <| by simp [_root_.pow_succ]).symm.trans h.modEq_zero_nat
rw [ke]
exact dvd_mul_of_dvd_right (((xy_coprime _ _).pow_left _).symm.dvd_of_dvd_mul_right this) _
