a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
suffices xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n from
  (lt_or_eq_of_le (Nat.le_of_succ_le_succ ij)).elim
    (fun h => lt_trans (eq_of_xn_modEq_lem1 h (le_of_lt jn)) this) fun h => by
    rw [h]; exact this
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
rw [Nat.mod_eq_of_lt (strictMono_x _ (Nat.lt_of_succ_lt jn)),
    Nat.mod_eq_of_lt (strictMono_x _ jn)]
no goals
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)
exact strictMono_x _ (Nat.lt_succ_self _)
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
rw [h]
no goals
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
exact this