Library Coq.Arith.Gt
Theorems about
gt
in
nat
.
This file is DEPRECATED now, see module
PeanoNat.Nat
instead, which favor
lt
over
gt
.
gt
is defined in
Init
/
Peano.v
as:
Definition gt (n m:nat) := m < n.
Require
Import
PeanoNat
Le
Lt
Plus
.
Local Open
Scope
nat_scope
.
Order and successor
Theorem
gt_Sn_O
n
:
S
n
>
0.
Theorem
gt_Sn_n
n
:
S
n
>
n
.
Theorem
gt_n_S
n
m
:
n
>
m
->
S
n
>
S
m
.
Lemma
gt_S_n
n
m
:
S
m
>
S
n
->
m
>
n
.
Theorem
gt_S
n
m
:
S
n
>
m
->
n
>
m
\/
m
=
n
.
Lemma
gt_pred
n
m
:
m
>
S
n
->
pred
m
>
n
.
Irreflexivity
Lemma
gt_irrefl
n
:
~
n
>
n
.
Asymmetry
Lemma
gt_asym
n
m
:
n
>
m
->
~
m
>
n
.
Relating strict and large orders
Lemma
le_not_gt
n
m
:
n
<=
m
->
~
n
>
m
.
Lemma
gt_not_le
n
m
:
n
>
m
->
~
n
<=
m
.
Theorem
le_S_gt
n
m
:
S
n
<=
m
->
m
>
n
.
Lemma
gt_S_le
n
m
:
S
m
>
n
->
n
<=
m
.
Lemma
gt_le_S
n
m
:
m
>
n
->
S
n
<=
m
.
Lemma
le_gt_S
n
m
:
n
<=
m
->
S
m
>
n
.
Transitivity
Theorem
le_gt_trans
n
m
p
:
m
<=
n
->
m
>
p
->
n
>
p
.
Theorem
gt_le_trans
n
m
p
:
n
>
m
->
p
<=
m
->
n
>
p
.
Lemma
gt_trans
n
m
p
:
n
>
m
->
m
>
p
->
n
>
p
.
Theorem
gt_trans_S
n
m
p
:
S
n
>
m
->
m
>
p
->
n
>
p
.
Comparison to 0
Theorem
gt_0_eq
n
:
n
>
0
\/
0
=
n
.
Simplification and compatibility
Lemma
plus_gt_reg_l
n
m
p
:
p
+
n
>
p
+
m
->
n
>
m
.
Lemma
plus_gt_compat_l
n
m
p
:
n
>
m
->
p
+
n
>
p
+
m
.
Hints
#[
global
]
Hint
Resolve
gt_Sn_O
gt_Sn_n
gt_n_S
:
arith
.
#[
global
]
Hint
Immediate
gt_S_n
gt_pred
:
arith
.
#[
global
]
Hint
Resolve
gt_irrefl
gt_asym
:
arith
.
#[
global
]
Hint
Resolve
le_not_gt
gt_not_le
:
arith
.
#[
global
]
Hint
Immediate
le_S_gt
gt_S_le
:
arith
.
#[
global
]
Hint
Resolve
gt_le_S
le_gt_S
:
arith
.
#[
global
]
Hint
Resolve
gt_trans_S
le_gt_trans
gt_le_trans
:
arith
.
#[
global
]
Hint
Resolve
plus_gt_compat_l
:
arith
.