Library Coq.Arith.Gt
Theorems about
gt
in
nat
.
gt
is defined in
Init
/Peano.
v
as:
Definition gt (n m:nat) := m < n.
Require
Import
Le
.
Require
Import
Lt
.
Require
Import
Plus
.
Open
Local
Scope
nat_scope
.
Implicit
Types
m
n
p
:
nat
.
Order and successor
Theorem
gt_Sn_O
:
forall
n
,
S
n
> 0.
Hint
Resolve
gt_Sn_O
:
arith
v62
.
Theorem
gt_Sn_n
:
forall
n
,
S
n
>
n
.
Hint
Resolve
gt_Sn_n
:
arith
v62
.
Theorem
gt_n_S
:
forall
n
m
,
n
>
m
->
S
n
>
S
m
.
Hint
Resolve
gt_n_S
:
arith
v62
.
Lemma
gt_S_n
:
forall
n
m
,
S
m
>
S
n
->
m
>
n
.
Hint
Immediate
gt_S_n
:
arith
v62
.
Theorem
gt_S
:
forall
n
m
,
S
n
>
m
->
n
>
m
\/
m
=
n
.
Lemma
gt_pred
:
forall
n
m
,
m
>
S
n
->
pred
m
>
n
.
Hint
Immediate
gt_pred
:
arith
v62
.
Irreflexivity
Lemma
gt_irrefl
:
forall
n
, ~
n
>
n
.
Hint
Resolve
gt_irrefl
:
arith
v62
.
Asymmetry
Lemma
gt_asym
:
forall
n
m
,
n
>
m
-> ~
m
>
n
.
Hint
Resolve
gt_asym
:
arith
v62
.
Relating strict and large orders
Lemma
le_not_gt
:
forall
n
m
,
n
<=
m
-> ~
n
>
m
.
Hint
Resolve
le_not_gt
:
arith
v62
.
Lemma
gt_not_le
:
forall
n
m
,
n
>
m
-> ~
n
<=
m
.
Hint
Resolve
gt_not_le
:
arith
v62
.
Theorem
le_S_gt
:
forall
n
m
,
S
n
<=
m
->
m
>
n
.
Hint
Immediate
le_S_gt
:
arith
v62
.
Lemma
gt_S_le
:
forall
n
m
,
S
m
>
n
->
n
<=
m
.
Hint
Immediate
gt_S_le
:
arith
v62
.
Lemma
gt_le_S
:
forall
n
m
,
m
>
n
->
S
n
<=
m
.
Hint
Resolve
gt_le_S
:
arith
v62
.
Lemma
le_gt_S
:
forall
n
m
,
n
<=
m
->
S
m
>
n
.
Hint
Resolve
le_gt_S
:
arith
v62
.
Transitivity
Theorem
le_gt_trans
:
forall
n
m
p
,
m
<=
n
->
m
>
p
->
n
>
p
.
Theorem
gt_le_trans
:
forall
n
m
p
,
n
>
m
->
p
<=
m
->
n
>
p
.
Lemma
gt_trans
:
forall
n
m
p
,
n
>
m
->
m
>
p
->
n
>
p
.
Theorem
gt_trans_S
:
forall
n
m
p
,
S
n
>
m
->
m
>
p
->
n
>
p
.
Hint
Resolve
gt_trans_S
le_gt_trans
gt_le_trans
:
arith
v62
.
Comparison to 0
Theorem
gt_O_eq
:
forall
n
,
n
> 0 \/ 0 =
n
.
Simplification and compatibility
Lemma
plus_gt_reg_l
:
forall
n
m
p
,
p
+
n
>
p
+
m
->
n
>
m
.
Lemma
plus_gt_compat_l
:
forall
n
m
p
,
n
>
m
->
p
+
n
>
p
+
m
.
Hint
Resolve
plus_gt_compat_l
:
arith
v62
.