a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
⊢ False
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
⊢ False
have co : Nat.coprime (yn a1 m) (xn a1 (m * (n / m))) :=
  Nat.coprime.symm <| (xy_coprime a1 _).coprime_dvd_right (y_mul_dvd a1 m (n / m))
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
m0 : 0 < m
⊢ False
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
⊢ False
have m0 : 0 < m :=
  m.eq_zero_or_pos.resolve_left fun e => by
    rw [e, Nat.mod_zero] at hp;rw [e] at h
    exact _root_.ne_of_lt (strictMono_y a1 hp) (eq_zero_of_zero_dvd h).symm
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))
hp : n % m > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
m0 : 0 < m
⊢ False
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
m0 : 0 < m
⊢ False
rw [← Nat.mod_add_div n m, yn_add] at h
no goals
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))
hp : n % m > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
m0 : 0 < m
⊢ False
exact
  not_le_of_gt (strictMono_y _ <| Nat.mod_lt n m0)
    (Nat.le_of_dvd (strictMono_y _ hp) <|
      co.dvd_of_dvd_mul_right <|
        (Nat.dvd_add_iff_right <| (y_mul_dvd _ _ _).mul_left _).2 h)
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
e : m = 0
⊢ False
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
e : m = 0
⊢ False
rw [e, Nat.mod_zero] at hp
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 0 ∣ yn a1 n
hp : n > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
e : m = 0
⊢ False
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
e : m = 0
⊢ False
rw [e] at h
no goals
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 0 ∣ yn a1 n
hp : n > 0
co : coprime (yn a1 m) (xn a1 (m * (n / m)))
e : m = 0
⊢ False
exact _root_.ne_of_lt (strictMono_y a1 hp) (eq_zero_of_zero_dvd h).symm
a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 (m * k)
a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 n
rw [e]
no goals
a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 (m * k)
apply y_mul_dvd