F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
⊢ (fun x => ↑x) m ≤ (fun x => ↑x) n
F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
⊢ Monotone fun x => ↑x
intro m n h
F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
m n : ℤ
h✝ : m ≤ n
h : 0 ≤ n - m
⊢ (fun x => ↑x) m ≤ (fun x => ↑x) n
F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
⊢ (fun x => ↑x) m ≤ (fun x => ↑x) n
rw [← sub_nonneg] at h
case intro
F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
k : ℕ
hk : ↑k = n - m
⊢ ↑m ≤ ↑n
F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
m n : ℤ
h✝ : m ≤ n
h : 0 ≤ n - m
⊢ (fun x => ↑x) m ≤ (fun x => ↑x) n
lift n - m to ℕ using h with k hk
case intro
F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑k
case intro
F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
k : ℕ
hk : ↑k = n - m
⊢ ↑m ≤ ↑n
rw [← sub_nonneg, ← cast_sub, ← hk, cast_ofNat]
no goals
case intro
F : Type ?u.9302
ι : Type ?u.9305
α : Type u_1
β : Type ?u.9311
inst✝ : OrderedRing α
m n : ℤ
h : m ≤ n
k : ℕ
hk : ↑k = n - m
⊢ 0 ≤ ↑k
exact k.cast_nonneg