Library Coq.Arith.Lt


Theorems about lt in nat. lt is defined in library Init/Peano.v as: 
Definition lt (n m:nat) := S n <= m.
Infix "<" := lt : nat_scope.

Require Import Le.
Local Open Scope nat_scope.

Implicit Types m n p : nat.

Irreflexivity


Theorem lt_irrefl : forall n, ~ n < n.
Hint Resolve lt_irrefl: arith v62.

Relationship between le and lt


Theorem lt_le_S : forall n m, n < m -> S n <= m.
Hint Immediate lt_le_S: arith v62.

Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m.
Hint Immediate lt_n_Sm_le: arith v62.

Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m.
Hint Immediate le_lt_n_Sm: arith v62.

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

Theorem lt_not_le : forall n m, n < m -> ~ m <= n.
Hint Immediate le_not_lt lt_not_le: arith v62.

Asymmetry


Theorem lt_asym : forall n m, n < m -> ~ m < n.

Order and successor


Theorem lt_n_Sn : forall n, n < S n.
Hint Resolve lt_n_Sn: arith v62.

Theorem lt_S : forall n m, n < m -> n < S m.
Hint Resolve lt_S: arith v62.

Theorem lt_n_S : forall n m, n < m -> S n < S m.
Hint Resolve lt_n_S: arith v62.

Theorem lt_S_n : forall n m, S n < S m -> n < m.
Hint Immediate lt_S_n: arith v62.

Theorem lt_0_Sn : forall n, 0 < S n.
Hint Resolve lt_0_Sn: arith v62.

Theorem lt_n_0 : forall n, ~ n < 0.
Hint Resolve lt_n_0: arith v62.

Predecessor


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

Lemma lt_pred : forall n m, S n < m -> n < pred m.
Hint Immediate lt_pred: arith v62.

Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n.
Hint Resolve lt_pred_n_n: arith v62.

Transitivity properties


Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.

Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.

Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.

Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62.

Large = strict or equal


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

Theorem le_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.

Theorem lt_le_weak : forall n m, n < m -> n <= m.
Hint Immediate lt_le_weak: arith v62.

Dichotomy


Theorem le_or_lt : forall n m, n <= m \/ m < n.

Theorem nat_total_order : forall n m, n <> m -> n < m \/ m < n.

Comparison to 0


Theorem neq_0_lt : forall n, 0 <> n -> 0 < n.
Hint Immediate neq_0_lt: arith v62.

Theorem lt_0_neq : forall n, 0 < n -> 0 <> n.
Hint Immediate lt_0_neq: arith v62.