(************************************************************************)
(*         *   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)         *)
(************************************************************************)

Fixpoint add (n m:nat) : nat :=
  match n with
  | O => m
  | S p => S (p + m)
  end
where "n + m" := (add n m) : nat_scope.

Require Import PeanoNat.

Local Open Scope nat_scope.

Notation plus_0_l := Nat.add_0_l (only parsing).
Notation plus_0_r := Nat.add_0_r (only parsing).
Notation plus_comm := Nat.add_comm (only parsing).
Notation plus_assoc := Nat.add_assoc (only parsing).

Notation plus_permute := Nat.add_shuffle3 (only parsing).

Definition plus_Snm_nSm : forall n m, S n + m = n + S m :=
 Peano.plus_n_Sm.

Lemma plus_assoc_reverse n m p : n + m + p = n + (m + p).
n, m, p:nat
n + m + p = n + (m + p)
Proof.
n, m, p:nat
n + m + p = n + (m + p)
  symmetry.
n, m, p:nat
n + (m + p) = n + m + p apply Nat.add_assoc.
Qed.

Lemma plus_reg_l n m p : p + n = p + m -> n = m.
n, m, p:nat
p + n = p + m -> n = m
Proof.
n, m, p:nat
p + n = p + m -> n = m
 apply Nat.add_cancel_l.
Qed.

Lemma plus_le_reg_l n m p : p + n <= p + m -> n <= m.
n, m, p:nat
p + n <= p + m -> n <= m
Proof.
n, m, p:nat
p + n <= p + m -> n <= m
 apply Nat.add_le_mono_l.
Qed.

Lemma plus_lt_reg_l n m p : p + n < p + m -> n < m.
n, m, p:nat
p + n < p + m -> n < m
Proof.
n, m, p:nat
p + n < p + m -> n < m
 apply Nat.add_lt_mono_l.
Qed.

Lemma plus_le_compat_l n m p : n <= m -> p + n <= p + m.
n, m, p:nat
n <= m -> p + n <= p + m
Proof.
n, m, p:nat
n <= m -> p + n <= p + m
 apply Nat.add_le_mono_l.
Qed.

Lemma plus_le_compat_r n m p : n <= m -> n + p <= m + p.
n, m, p:nat
n <= m -> n + p <= m + p
Proof.
n, m, p:nat
n <= m -> n + p <= m + p
 apply Nat.add_le_mono_r.
Qed.

Lemma plus_lt_compat_l n m p : n < m -> p + n < p + m.
n, m, p:nat
n < m -> p + n < p + m
Proof.
n, m, p:nat
n < m -> p + n < p + m
 apply Nat.add_lt_mono_l.
Qed.

Lemma plus_lt_compat_r n m p : n < m -> n + p < m + p.
n, m, p:nat
n < m -> n + p < m + p
Proof.
n, m, p:nat
n < m -> n + p < m + p
 apply Nat.add_lt_mono_r.
Qed.

Lemma plus_le_compat n m p q : n <= m -> p <= q -> n + p <= m + q.
n, m, p, q:nat
n <= m -> p <= q -> n + p <= m + q
Proof.
n, m, p, q:nat
n <= m -> p <= q -> n + p <= m + q
 apply Nat.add_le_mono.
Qed.

Lemma plus_le_lt_compat n m p q : n <= m -> p < q -> n + p < m + q.
n, m, p, q:nat
n <= m -> p < q -> n + p < m + q
Proof.
n, m, p, q:nat
n <= m -> p < q -> n + p < m + q
 apply Nat.add_le_lt_mono.
Qed.

Lemma plus_lt_le_compat n m p q : n < m -> p <= q -> n + p < m + q.
n, m, p, q:nat
n < m -> p <= q -> n + p < m + q
Proof.
n, m, p, q:nat
n < m -> p <= q -> n + p < m + q
 apply Nat.add_lt_le_mono.
Qed.

Lemma plus_lt_compat n m p q : n < m -> p < q -> n + p < m + q.
n, m, p, q:nat
n < m -> p < q -> n + p < m + q
Proof.
n, m, p, q:nat
n < m -> p < q -> n + p < m + q
 apply Nat.add_lt_mono.
Qed.

Lemma le_plus_l n m : n <= n + m.
n, m:nat
n <= n + m
Proof.
n, m:nat
n <= n + m
 apply Nat.le_add_r.
Qed.

Lemma le_plus_r n m : m <= n + m.
n, m:nat
m <= n + m
Proof.
n, m:nat
m <= n + m
 rewrite Nat.add_comm.
n, m:nat
m <= m + n apply Nat.le_add_r.
Qed.

Theorem le_plus_trans n m p : n <= m -> n <= m + p.
n, m, p:nat
n <= m -> n <= m + p
Proof.
n, m, p:nat
n <= m -> n <= m + p
  intros.
n, m, p:nat
H:n <= m
n <= m + p now rewrite <- Nat.le_add_r.
Qed.

Theorem lt_plus_trans n m p : n < m -> n < m + p.
n, m, p:nat
n < m -> n < m + p
Proof.
n, m, p:nat
n < m -> n < m + p
  intros.
n, m, p:nat
H:n < m
n < m + p apply Nat.lt_le_trans with m.
n, m, p:nat
H:n < m
n < m
n, m, p:nat
H:n < m
m <= m + p trivial.
n, m, p:nat
H:n < m
m <= m + p apply Nat.le_add_r.
Qed.

Lemma plus_is_O n m : n + m = 0 -> n = 0 /\ m = 0.
n, m:nat
n + m = 0 -> n = 0 /\ m = 0
Proof.
n, m:nat
n + m = 0 -> n = 0 /\ m = 0
  destruct n; now split.
Qed.

Definition plus_is_one m n :
  m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}.
m, n:nat
m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}
Proof.
m, n:nat
m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}
  destruct m as [| m]; auto.
m, n:nat
S m + n = 1 -> {S m = 0 /\ n = 1} + {S m = 1 /\ n = 0}
  destruct m; auto.
m, n:nat
S (S m) + n = 1 ->
{S (S m) = 0 /\ n = 1} + {S (S m) = 1 /\ n = 0}
  discriminate.
Defined.

Notation plus_permute_2_in_4 := Nat.add_shuffle1 (only parsing).

Fixpoint tail_plus n m : nat :=
  match n with
    | O => m
    | S n => tail_plus n (S m)
  end.

Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
forall n m : nat, n + m = tail_plus n m
Proof.
forall n m : nat, n + m = tail_plus n m
induction n as [| n IHn]; simpl; auto.
n:nat
IHn:forall m : nat, n + m = tail_plus n m
forall m : nat, S (n + m) = tail_plus n (S m)
intro m; rewrite <- IHn; simpl; auto.
Qed.

Lemma succ_plus_discr n m : n <> S (m+n).
n, m:nat
n <> S (m + n)
Proof.
n, m:nat
n <> S (m + n)
 apply Nat.succ_add_discr.
Qed.

Lemma n_SSn n : n <> S (S n).
n:nat
n <> S (S n)
Proof (succ_plus_discr n 1).

Lemma n_SSSn n : n <> S (S (S n)).
n:nat
n <> S (S (S n))
Proof (succ_plus_discr n 2).

Lemma n_SSSSn n : n <> S (S (S (S n))).
n:nat
n <> S (S (S (S n)))
Proof (succ_plus_discr n 3).

Hint Immediate plus_comm : arith.
Hint Resolve plus_assoc plus_assoc_reverse : arith.
Hint Resolve plus_le_compat_l plus_le_compat_r : arith.
Hint Resolve le_plus_l le_plus_r le_plus_trans : arith.
Hint Immediate lt_plus_trans : arith.
Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith.

Require Import Le Lt.