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
).
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
.
Theorem
le_lt_n_Sm
n
m
:
n
<=
m
->
n
<
S
m
.
Hint Immediate
lt_le_S
:
arith
.
Hint Immediate
lt_n_Sm_le
:
arith
.
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
.
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
.
Hint Resolve
lt_0_Sn
lt_n_0
:
arith
.
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
.
Hint Resolve
lt_n_Sn
lt_S
lt_n_S
:
arith
.
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
.
Hint Immediate
lt_pred
:
arith
.
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
).
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
).
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
.