Documentation

Mathlib.Data.Int.SuccPred

Successors and predecessors of integers #

In this file, we show that is both an archimedean SuccOrder and an archimedean PredOrder.

@[reducible, inline]
Equations
    @[reducible, inline]
    Equations

      Covering relation #

      @[simp]
      theorem Int.natCast_covBy {a b : } :
      a b a b
      theorem CovBy.intCast {a b : } :
      a ba b

      Alias of the reverse direction of Int.natCast_covBy.