Library Coq.Arith.Compare

Local Open Scope nat_scope.

Notation not_eq_sym := not_eq_sym (only parsing).

Implicit Types m n p q : nat.

Require Import Arith_base.
Require Import Peano_dec.
Require Import Compare_dec.

Definition le_or_le_S := le_le_S_dec.

Definition Pcompare := gt_eq_gt_dec.

Lemma le_dec : forall n m, {n <= m} + {m <= n}.

Definition lt_or_eq n m := {m > n} + {n = m}.

Lemma le_decide : forall n m, n <= m -> lt_or_eq n m.

Lemma le_le_S_eq : forall n m, n <= m -> S n <= m \/ n = m.

Lemma discrete_nat :
  forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))).

Require Export Wf_nat.