Γ : Type ?u.2177048
R : Type ?u.2177051
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
x : PowerSeries R
⊢ ∀ {a b : ℕ}, ↑a ≤ ↑b ↔ a ≤ b
Γ : Type ?u.2177048
R : Type ?u.2177051
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
x : PowerSeries R
⊢ ∀ {a b : ℕ},
    ↑{ toFun := Nat.cast, inj' := (_ : Injective Nat.cast) } a ≤
        ↑{ toFun := Nat.cast, inj' := (_ : Injective Nat.cast) } b ↔
      a ≤ b
simp only [Function.Embedding.coeFn_mk]
no goals
Γ : Type ?u.2177048
R : Type ?u.2177051
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
x : PowerSeries R
⊢ ∀ {a b : ℕ}, ↑a ≤ ↑b ↔ a ≤ b
exact Nat.cast_le