(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************)
(*           The Calculus of Inductive Constructions            *)
(*                       COQ v5.10                              *)
(*                                                              *)
(* Laurent Arditi.  Laboratoire I3S. CNRS ura 1376.             *)
(* Universite de Nice - Sophia Antipolis                        *)
(* arditi@unice.fr, http://wwwi3s.unice.fr/~arditi/lolo.html    *)
(*                                                              *)
(* date: may 1995                                               *)
(* file: Arith_compl.v                                          *)
(* contents: additionnal lemmas on plus,mult,minus,le...        *)
(* definitions of 2^ and factorial, lemmas about them           *)
(****************************************************************)


Require Export Plus.
Require Export Mult.
Require Import Minus.
Require Export Lt.
Require Export Le.
Require Export Gt.

(****************************************************************)
(* Complements sur plus et mult *)

Lemma plus_n_SO : forall x : nat, x + 1 = S x.
(* Goal: forall x : nat, @eq nat (Nat.add x (S O)) (S x) *)
intros; rewrite plus_comm; auto with arith.
Qed. Hint Resolve plus_n_SO.

Lemma plus_permute2 : forall x y z : nat, x + y + z = x + z + y.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros.
(* Goal: @eq nat (Nat.add (Nat.add x y) z) (Nat.add (Nat.add x z) y) *)
rewrite (plus_comm x y).
(* Goal: @eq nat (Nat.add (PeanoNat.Nat.add y x) z) (Nat.add (Nat.add x z) y) *)
rewrite (plus_comm x z).
(* Goal: @eq nat (Nat.add (PeanoNat.Nat.add z x) y) (PeanoNat.Nat.add z (PeanoNat.Nat.add y x)) *)
rewrite plus_comm.
symmetry  in |- *.
(* Goal: @eq nat (Nat.add (PeanoNat.Nat.add z x) y) (PeanoNat.Nat.add z (PeanoNat.Nat.add y x)) *)
rewrite plus_comm.
(* Goal: @eq nat (PeanoNat.Nat.add y (PeanoNat.Nat.add z x)) (PeanoNat.Nat.add z (PeanoNat.Nat.add y x)) *)
rewrite plus_permute.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
auto with arith.
Qed. Hint Resolve plus_permute2.

Lemma mult_sym : forall a b : nat, a * b = b * a.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros a b; elim a; simpl in |- *; auto with arith.
(* Goal: forall (n : nat) (_ : @eq nat (Nat.mul n b) (Nat.mul b n)), @eq nat (Nat.add b (Nat.mul n b)) (Nat.mul b (S n)) *)
intros y H.
(* Goal: @eq nat (Nat.add b (Nat.mul y b)) (Nat.mul b (S y)) *)
replace (y * b) with (b * y).
(* Goal: @eq nat (Nat.add b (Nat.mul b y)) (Nat.mul b (S y)) *)
elim (mult_n_Sm b y).
(* Goal: @eq nat (Nat.add b (Nat.mul b y)) (Nat.add (Nat.mul b y) b) *)
apply plus_comm.
Qed. Hint Resolve mult_sym.

Lemma mult_permute : forall a b c : nat, a * b * c = a * c * b.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros.
(* Goal: @eq nat (Nat.mul a (Nat.mul b c)) (Nat.mul (Nat.mul a c) b) *)
rewrite mult_assoc_reverse.
(* Goal: @eq nat (Nat.mul a (Nat.mul b c)) (Nat.mul (Nat.mul a c) b) *)
rewrite mult_assoc_reverse.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
replace (c * b) with (b * c); auto with arith.
Qed. Hint Resolve mult_permute.

(*
Lemma plus_n_n : (n:nat)((plus n n)=(mult n (S (S O)))).
Intro.
Rewrite -> mult_sym.
Simpl.
Replace (plus n O) with (plus O n);Auto with arith.
Qed. Hints Resolve plus_n_n.
*)

Lemma plus_O_O : forall n m : nat, n + m = 0 -> n = 0.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction n. intros. trivial with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. inversion H0.
Qed.

Lemma mult_plus_distr2 : forall n m p : nat, n * (m + p) = n * m + n * p.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. rewrite mult_sym. rewrite mult_plus_distr_r. rewrite mult_sym.
(* Goal: @eq nat (Nat.sub a (Nat.sub a (S n))) (Nat.sub a (Nat.sub a (S n))) *)
replace (p * n) with (n * p). trivial with arith. apply mult_sym.
Qed.

(****************************************************************)
(* La fonction puissance de 2 *)

Fixpoint power2 (n : nat) : nat :=
  match n with
  | O => 1
  | S x => power2 x + power2 x
  end.

Lemma power2_eq2 : forall x : nat, power2 (S x) = power2 x + power2 x.
Proof. 
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
 auto with arith.
Qed.


(*
Lemma power2_SO : ((S (S O))=(power2 (S O))).
Auto with arith. Qed. Hints Resolve power2_SO.

Lemma mult_power2 : (x,y:nat)
		((mult (power2 x) (power2 y))=(power2 (plus x y))).
*)
Lemma power2_plus : forall x y : nat, power2 (x + y) = power2 x * power2 y.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction x. intros. simpl in |- *. elim plus_n_O; auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. simpl in |- *. rewrite H. rewrite mult_plus_distr_r. trivial with arith.
Qed.

(****************************************************************)
(* Complements sur Lt Le Gt... *)

Theorem le_plus_n_m : forall n m : nat, n <= m -> n + n <= m + m.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction n. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. inversion H0. auto with arith.
(* Goal: le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simpl in |- *. elim plus_n_Sm. elim plus_n_Sm.
(* Goal: le (S (Nat.add n0 n0)) (S (Nat.add m0 m0)) *)
apply le_n_S. apply le_n_S. apply H. apply le_Sn_le. exact H1.
Qed. Hint Resolve le_plus_n_m.

Theorem lt_plus_n_m : forall n m : nat, n < m -> S (n + n) < m + m.
(* Goal: forall n : nat, @eq nat (Nat.sub n (S O)) (Nat.pred n) *)
simple induction n.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simpl in |- *. simple induction m. simpl in |- *. intros. absurd (0 < 0). apply le_not_lt. auto with arith.
(* Goal: le (Nat.sub a n) a *)
exact H.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. simpl in |- *. elim plus_n_Sm. apply lt_n_S. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. inversion H0. simpl in |- *. repeat elim plus_n_Sm. auto with arith.
(* Goal: le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simpl in |- *.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
repeat elim plus_n_Sm. apply lt_n_S. apply lt_n_S. apply H. inversion H1. auto with arith.
(* Goal: le n a *)
(* Goal: le (S n) a *)
(* Goal: le (S (Nat.sub a (S n))) a *)
(* Goal: @eq nat (Nat.sub (S a) (S (Nat.sub a (S n)))) (Nat.sub a (Nat.sub a (S n))) *)
apply le_lt_n_Sm. apply le_Sn_le. apply le_Sn_le. exact H3.
Qed.

Lemma le_plus_lem1 : forall a b c : nat, a <= b -> c + a <= c + b.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. inversion H. auto with arith.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
elim plus_n_Sm. apply le_S. auto with arith.
Qed. Hint Resolve le_plus_lem1.

Lemma le_plus_lem2 : forall a b c : nat, c + a <= c + b -> a <= b.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction c. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simpl in |- *. intros. apply H. apply le_S_n. exact H0.
Qed.

Lemma gt_double : forall a b : nat, a + a > b + b -> a > b. 
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction a. simpl in |- *. intros. absurd (0 > b + b). auto with arith.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
auto with arith. simple induction b. simpl in |- *. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. apply gt_n_S.
(* Goal: le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
apply H. generalize H1. simpl in |- *. elim plus_n_Sm. elim plus_n_Sm. intro.
(* Goal: le (S n1) (S n0) *)
cut (S (n + n) > S (n0 + n0)). intro. apply gt_S_n. exact H3.
(* Goal: gt n n0 *)
apply gt_S_n. exact H2.
Qed.

Lemma gt_double_inv : forall a b : nat, a > b -> a + a > b + b.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction a. intros. absurd (0 > b). auto with arith. exact H.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction b. intros. simpl in |- *. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. simpl in |- *. elim plus_n_Sm.
(* Goal: gt (Nat.add n n) (Nat.add n0 (S n0)) *)
elim plus_n_Sm. apply gt_n_S. apply gt_n_S. apply H. apply gt_S_n. exact H1.
Qed.

Lemma gt_double_n_S : forall a b : nat, a > b -> a + a > S (b + b).
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction a. intros. absurd (0 > b). auto with arith.
(* Goal: le (Nat.sub a n) a *)
exact H.
(* Goal: le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction b. simpl in |- *. intro.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
apply gt_n_S. unfold gt in |- *. unfold lt in |- *. elim plus_n_Sm. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. simpl in |- *. apply gt_n_S.
(* Goal: gt (Nat.add n n) (Nat.add n0 (S n0)) *)
elim plus_n_Sm. apply gt_n_S. elim plus_n_Sm. apply H. apply gt_S_n. exact H1.
Qed.

Lemma gt_double_S_n : forall a b : nat, a > b -> S (a + a) > b + b.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. apply gt_trans with (a + a). auto with arith. apply gt_double_inv. exact H.
Qed.

(****************************************************************)
(* Complements sur minus *)

Lemma minus_le_O : forall a b : nat, a <= b -> a - b = 0.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. pattern a, b in |- *. apply le_elim_rel. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. simpl in |- *. exact H1.
(* Goal: le (Nat.sub a n) a *)
exact H.
Qed.

Lemma minus_n_SO : forall n : nat, n - 1 = pred n.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction n. auto with arith. intros. simpl in |- *. auto with arith.
Qed.

Lemma minus_le_lem2c : forall a b : nat, a - S b <= a - b.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. pattern a, b in |- *. apply nat_double_ind. auto with arith.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intro. elim minus_n_O. rewrite minus_n_SO. simpl in |- *. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. simpl in |- *. exact H.
Qed.

Lemma minus_le_lem2 : forall a b : nat, a - b <= a.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction b. elim minus_n_O. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. apply le_trans with (a - n). apply minus_le_lem2c.
(* Goal: le (Nat.sub a n) a *)
exact H.
Qed. Hint Resolve minus_le_lem2.

Lemma minus_minus_lem1 : forall a b : nat, a - b - a = 0.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. apply minus_le_O. apply minus_le_lem2.
Qed. Hint Resolve minus_minus_lem1.

Lemma minus_minus_lem2 : forall a b : nat, b <= a -> a - (a - b) = b.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction b. intros. elim minus_n_O. elim minus_n_n. trivial with arith. intros.
(* Goal: @eq nat (Nat.sub a (Nat.sub a (S n))) (S n) *)
replace (a - (a - S n)) with (S a - S (a - S n)).
(* Goal: @eq nat (Nat.sub (S a) (S (Nat.sub a (S n)))) (S n) *)
(* Goal: @eq nat (Nat.sub (S a) (S (Nat.sub a (S n)))) (Nat.sub a (Nat.sub a (S n))) *)
rewrite <- (minus_Sn_m a (S (a - S n))). rewrite (minus_Sn_m a (S n)).
(* Goal: @eq nat (Nat.sub a (Nat.sub a (S n))) (Nat.sub a (Nat.sub a (S n))) *)
simpl in |- *. rewrite <- H. rewrite H. rewrite H. trivial with arith.
(* Goal: le n a *)
(* Goal: le (S n) a *)
(* Goal: le (S (Nat.sub a (S n))) a *)
(* Goal: @eq nat (Nat.sub (S a) (S (Nat.sub a (S n)))) (Nat.sub a (Nat.sub a (S n))) *)
apply le_Sn_le. exact H0.
(* Goal: le n a *)
(* Goal: le (S n) a *)
(* Goal: le (S (Nat.sub a (S n))) a *)
(* Goal: @eq nat (Nat.sub (S a) (S (Nat.sub a (S n)))) (Nat.sub a (Nat.sub a (S n))) *)
apply le_Sn_le. exact H0. apply le_Sn_le. exact H0. exact H0.
(* Goal: @eq nat (Nat.sub a (Nat.sub a (S n))) (Nat.sub a (Nat.sub a (S n))) *)
rewrite minus_Sn_m. simpl in |- *. apply minus_le_lem2. exact H0. simpl in |- *. trivial with arith.
Qed.

Lemma le_minus_minus : forall a b c : nat, c <= b -> a - b <= a - c.
(* Goal: not (le (S n0) O) *)
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
simple induction a. simpl in |- *. auto with arith.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. generalize H0. elim c. elim minus_n_O. intro. apply minus_le_lem2.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
elim b. intros. absurd (S n0 <= 0). auto with arith.
(* Goal: le (S n0) O *)
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
exact H2.
(* Goal: forall (n0 : nat) (_ : forall (n1 : nat) (_ : forall _ : le n1 n0, le (Nat.sub (S n) n0) (Nat.sub (S n) n1)) (_ : le (S n1) n0), le (Nat.sub (S n) n0) (Nat.sub (S n) (S n1))) (n1 : nat) (_ : forall _ : le n1 (S n0), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) n1)) (_ : le (S n1) (S n0)), le (Nat.sub (S n) (S n0)) (Nat.sub (S n) (S n1)) *)
intros. simpl in |- *. apply H. apply le_S_n. exact H3.
Qed.
