Library Coq.Arith.Lt


Strict order on natural numbers.
This file is mostly OBSOLETE now, see module PeanoNat.Nat instead.
lt is defined in library Init/Peano.v as: 
Definition lt (n m:nat) := S n <= m.
Infix "<" := lt : nat_scope.

Require Import PeanoNat.

Local Open Scope nat_scope.

Irreflexivity


Notation lt_irrefl := Nat.lt_irrefl (only parsing).
#[global]
Hint Resolve lt_irrefl: arith.

Relationship between le and lt


Theorem lt_le_S n m : n < m -> S n <= m.

Theorem lt_n_Sm_le n m : n < S m -> n <= m.

Register lt_n_Sm_le as num.nat.lt_n_Sm_le.

Theorem le_lt_n_Sm n m : n <= m -> n < S m.

Register le_lt_n_Sm as num.nat.le_lt_n_Sm.

#[global]
Hint Immediate lt_le_S: arith.
#[global]
Hint Immediate lt_n_Sm_le: arith.
#[global]
Hint Immediate le_lt_n_Sm: arith.

Theorem le_not_lt n m : n <= m -> ~ m < n.

Theorem lt_not_le n m : n < m -> ~ m <= n.

#[global]
Hint Immediate le_not_lt lt_not_le: arith.

Asymmetry


Notation lt_asym := Nat.lt_asymm (only parsing).

Order and 0


Notation lt_0_Sn := Nat.lt_0_succ (only parsing). Notation lt_n_0 := Nat.nlt_0_r (only parsing).
Theorem neq_0_lt n : 0 <> n -> 0 < n.

Theorem lt_0_neq n : 0 < n -> 0 <> n.

#[global]
Hint Resolve lt_0_Sn lt_n_0 : arith.
#[global]
Hint Immediate neq_0_lt lt_0_neq: arith.

Order and successor


Notation lt_n_Sn := Nat.lt_succ_diag_r (only parsing). Notation lt_S := Nat.lt_lt_succ_r (only parsing).
Theorem lt_n_S n m : n < m -> S n < S m.

Theorem lt_S_n n m : S n < S m -> n < m.

Register lt_S_n as num.nat.lt_S_n.

#[global]
Hint Resolve lt_n_Sn lt_S lt_n_S : arith.
#[global]
Hint Immediate lt_S_n : arith.

Predecessor


Lemma S_pred n m : m < n -> n = S (pred n).

Lemma S_pred_pos n: O < n -> n = S (pred n).

Lemma lt_pred n m : S n < m -> n < pred m.

Lemma lt_pred_n_n n : 0 < n -> pred n < n.

#[global]
Hint Immediate lt_pred: arith.
#[global]
Hint Resolve lt_pred_n_n: arith.

Transitivity properties


Notation lt_trans := Nat.lt_trans (only parsing).
Notation lt_le_trans := Nat.lt_le_trans (only parsing).
Notation le_lt_trans := Nat.le_lt_trans (only parsing).

Register le_lt_trans as num.nat.le_lt_trans.

#[global]
Hint Resolve lt_trans lt_le_trans le_lt_trans: arith.

Large = strict or equal


Notation le_lt_or_eq_iff := Nat.lt_eq_cases (only parsing).

Theorem le_lt_or_eq n m : n <= m -> n < m \/ n = m.

Notation lt_le_weak := Nat.lt_le_incl (only parsing).

#[global]
Hint Immediate lt_le_weak: arith.

Dichotomy


Notation le_or_lt := Nat.le_gt_cases (only parsing).
Theorem nat_total_order n m : n <> m -> n < m \/ m < n.


For compatibility, we "Require" the same files as before

Require Import Le.