Data.Nat.Order

Implementation of ordering relations for `Nat`ural numbers

Definitions

zeroNeverGreater : Not (LTE (S n) 0)

Totality: total
Visibility: public export

zeroAlwaysSmaller : LTE 0 n

Totality: total
Visibility: public export

ltesuccinjective : Not (LTE n m) -> Not (LTE (S n) (S m))

Totality: total
Visibility: public export

decideLTBounded : {0 p : Nat -> Type} -> ((n : Nat) -> Dec (p n)) -> (n : Nat) -> Dec ((k : Nat) -> LT k n -> p k)

  If a predicate is decidable then we can decide whether it holds on
  a bounded domain.

Totality: total
Visibility: public export

decideLTEBounded : {0 p : Nat -> Type} -> ((n : Nat) -> Dec (p n)) -> (n : Nat) -> Dec ((k : Nat) -> LTE k n -> p k)

  If a predicate is decidable then we can decide whether it holds on
  a bounded domain.

Totality: total
Visibility: public export

lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)

Totality: total
Visibility: public export

shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)

Totality: total
Visibility: public export