/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
Ported by: Scott Morrison

! This file was ported from Lean 3 source module algebra.order.ring.char_zero
! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.CharZero.Defs
import Mathlib.Algebra.Order.Ring.Defs

/-!
# Strict ordered semiring have characteristic zero
-/


variable {
α: Type ?u.5
α : 
Type _: Type (?u.2+1)
Type _}

-- see Note [lower instance priority]
instance (priority := 100) 
StrictOrderedSemiring.to_charZero: ∀ {α : Type u_1} [inst : StrictOrderedSemiring α], CharZero α
StrictOrderedSemiring.to_charZero [
StrictOrderedSemiring: Type ?u.8 → Type ?u.8
StrictOrderedSemiring 
α: Type ?u.5
α] :
    
CharZero: (R : Type ?u.11) → [inst : AddMonoidWithOne R] → Prop
CharZero 
α: Type ?u.5
α :=
  ⟨
StrictMono.injective: ∀ {α : Type ?u.138} {β : Type ?u.137} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → Function.Injective f
StrictMono.injective <|
      
strictMono_nat_of_lt_succ: ∀ {α : Type ?u.186} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f n < f (n + 1)) → StrictMono f
strictMono_nat_of_lt_succ fun 
n: ?m.226
n => by
Goals accomplished! 🐙
        
α: Type ?u.5

inst✝: StrictOrderedSemiring α

n: ℕ

↑n < ↑(n + 1)rw [
α: Type ?u.5

inst✝: StrictOrderedSemiring α

n: ℕ

↑n < ↑(n + 1)
Nat.cast_succ: ∀ {R : Type ?u.354} [inst : AddMonoidWithOne R] (n : ℕ), ↑(Nat.succ n) = ↑n + 1
Nat.cast_succ
α: Type ?u.5

inst✝: StrictOrderedSemiring α

n: ℕ

↑n < ↑n + 1]
α: Type ?u.5

inst✝: StrictOrderedSemiring α

n: ℕ

↑n < ↑n + 1
        
α: Type ?u.5

inst✝: StrictOrderedSemiring α

n: ℕ

↑n < ↑(n + 1)apply 
lt_add_one: ∀ {α : Type ?u.397} [inst : One α] [inst_1 : AddZeroClass α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
  [inst_4 : NeZero 1] [inst_5 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α), a < a + 1
lt_add_one
Goals accomplished! 🐙⟩
#align strict_ordered_semiring.to_char_zero 
StrictOrderedSemiring.to_charZero: ∀ {α : Type u_1} [inst : StrictOrderedSemiring α], CharZero α
StrictOrderedSemiring.to_charZero