Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
Order on natural numbers.
This file is mostly OBSOLETE now, see module PeanoNat.Nat instead.
le is defined in Init/Peano.v as: 
Inductive le (n:nat) : nat -> Prop :=
  | le_n : n <= n
  | le_S : forall m:nat, n <= m -> n <= S m

where "n <= m" := (le n m) : nat_scope.

Require Import PeanoNat.

Local Open Scope nat_scope.

le is an order on nat

Notation le_refl := Nat.le_refl (only parsing).
Notation le_trans := Nat.le_trans (only parsing).
Notation le_antisym := Nat.le_antisymm (only parsing).

Hint Resolve le_trans: arith.
Hint Immediate le_antisym: arith.

Properties of le w.r.t 0

Notation le_0_n := Nat.le_0_l (only parsing).  (* 0 <= n *)
Notation le_Sn_0 := Nat.nle_succ_0 (only parsing).  (* ~ S n <= 0 *)


n:nat
n <= 0 -> 0 = n


n:nat
n <= 0 -> 0 = n

 
n:nat
H:n <= 0
0 = n
 
n:nat
H:n <= 0
n = 0
 now apply Nat.le_0_r.
Qed.

Properties of le w.r.t successor

See also Nat.succ_le_mono. 
forall n m : nat, n <= m -> S n <= S m

Proof Peano.le_n_S.


forall n m : nat, S n <= S m -> n <= m

Proof Peano.le_S_n.

Notation le_n_Sn := Nat.le_succ_diag_r (only parsing). (* n <= S n *)
Notation le_Sn_n := Nat.nle_succ_diag_l (only parsing). (* ~ S n <= n *)


forall n m : nat, S n <= m -> n <= m

Proof Nat.lt_le_incl.

Hint Resolve le_0_n le_Sn_0: arith.
Hint Resolve le_n_S le_n_Sn le_Sn_n : arith.
Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith.

Properties of le w.r.t predecessor

Notation le_pred_n := Nat.le_pred_l (only parsing). (* pred n <= n *)
Notation le_pred := Nat.pred_le_mono (only parsing). (* n<=m -> pred n <= pred m *)

Hint Resolve le_pred_n: arith.

A different elimination principle for the order on natural numbers

forall P : nat -> nat -> Prop,
(forall p : nat, P 0 p) ->
(forall p q : nat, p <= q -> P p q -> P (S p) (S q)) ->
forall n m : nat, n <= m -> P n m


forall P : nat -> nat -> Prop,
(forall p : nat, P 0 p) ->
(forall p q : nat, p <= q -> P p q -> P (S p) (S q)) ->
forall n m : nat, n <= m -> P n m

  
P:nat -> nat -> Prop
H0:forall p : nat, P 0 p
HS:forall p q : nat,
p <= q -> P p q -> P (S p) (S q)
forall n m : nat, n <= m -> P n m

  
P:nat -> nat -> Prop
H0:forall p : nat, P 0 p
HS:forall p q : nat,
p <= q -> P p q -> P (S p) (S q)
n:nat
IHn:forall m : nat, n <= m -> P n m
forall m : nat, S n <= m -> P (S n) m

  
P:nat -> nat -> Prop
H0:forall p : nat, P 0 p
HS:forall p q : nat,
p <= q -> P p q -> P (S p) (S q)
n:nat
IHn:forall m0 : nat, n <= m0 -> P n m0
m:nat
Le:S n <= m
P (S n) m
 elim Le; auto with arith.
 Qed.

(* begin hide *)
Notation le_O_n := le_0_n (only parsing).
Notation le_Sn_O := le_Sn_0 (only parsing).
Notation le_n_O_eq := le_n_0_eq (only parsing).
(* end hide *)