(* Copyright (C) 2005-2008 Sebastien Briais *)
(* http://lamp.epfl.ch/~sbriais/ *)

(* This library 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 library 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 *)
(* Lesser General Public License for more details. *)

(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this library; if not, write to the Free Software *)
(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)

Require Export Arith.
Require Export ArithRing.
Require Export Omega.

Unset Standard Proposition Elimination Names.

(** We first begin with some lemmas that relates *)
(** +, * and - that are not in the standard library *)
Lemma mult_lemma1 : forall (n m:nat),(n <> O)->(m <> 0)->(n <= n*m).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: lt n (Init.Nat.mul n m) *)
  rewrite mult_comm.
(* Goal: le n (Nat.mul m n) *)
  induction m;simpl;auto with arith.
(* Goal: le n O *)
  elim H0;trivial.
Qed.

Lemma mult_lemma2 : forall (n m:nat),(n*m = O)->(n=O)\/(m=O).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: or (@eq nat n O) (@eq nat m O) *)
  induction n.
(* Goal: or (@eq nat O O) (@eq nat m O) *)
(* Goal: or (@eq nat (S n) O) (@eq nat m O) *)
  tauto.
(* Goal: @eq nat (S m) (S O) *)
  simpl in H.
(* Goal: or (@eq nat (S n0) O) (@eq nat m (S O)) *)
  right.
(* Goal: @eq nat m O *)
  assert (m <= O);try omega.
(* Goal: le m O *)
  rewrite <- H.
(* Goal: @eq nat (Init.Nat.sub x O) x *)
(* Goal: @eq nat (Init.Nat.sub (Nat.add y x) y) x *)
  auto with arith.
Qed.

Lemma mult_lemma3 : forall (n m:nat),(n <> O)->(m > 1)->(n < n*m).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: lt n (Init.Nat.mul n m) *)
  rewrite mult_comm.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat m (S O)) *)
  induction m.
(* Goal: lt n (Nat.mul O n) *)
(* Goal: lt n (Nat.mul (S m) n) *)
  inversion H0.
(* Goal: @eq nat (Init.Nat.mul a n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  simpl.
(* Goal: lt n (Nat.add n (Nat.mul m n)) *)
  assert (O < m*n);try omega.
(* Goal: lt O (Init.Nat.mul m n) *)
  inversion H0;try omega.
(* Goal: lt O (Init.Nat.mul m n) *)
  assert (1 <= n);try omega.
(* Goal: lt O (Init.Nat.mul m n) *)
  assert (m > 1);try omega.
(* Goal: lt O (Init.Nat.mul m n) *)
  generalize (IHm H4);omega.
Qed.

Lemma mult_lemma4 : forall (n m:nat),n=n*m -> n=O \/ m=1.
(* Goal: forall (n m : nat) (_ : @eq nat n (Init.Nat.mul n m)), or (@eq nat n O) (@eq nat m (S O)) *)
  intros n m.
(* Goal: forall _ : @eq nat n (Init.Nat.mul n m), or (@eq nat n O) (@eq nat m (S O)) *)
  case n.
(* Goal: forall _ : @eq nat O (Init.Nat.mul O m), or (@eq nat O O) (@eq nat m (S O)) *)
(* Goal: forall (n : nat) (_ : @eq nat (S n) (Init.Nat.mul (S n) m)), or (@eq nat (S n) O) (@eq nat m (S O)) *)
  left;trivial.
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: or (@eq nat (S n0) O) (@eq nat m (S O)) *)
  right.
(* Goal: @eq nat m (S O) *)
  destruct m.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat O (S O)) *)
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  rewrite mult_comm in H.
(* Goal: @eq nat O (S O) *)
(* Goal: @eq nat (S m) (S O) *)
  discriminate.
(* Goal: @eq nat (S m) (S O) *)
  destruct m;trivial.
(* Goal: @eq nat (S (S m)) (S O) *)
  assert ((S n0)<(S n0)*(S (S m))).
(* Goal: @eq nat (Init.Nat.sub x O) x *)
(* Goal: @eq nat (Init.Nat.sub (Nat.add y x) y) x *)
  apply mult_lemma3;intros;auto with arith.
(* Goal: @eq nat (S (S m)) (S O) *)
  rewrite <- H in H0.
(* Goal: @eq nat (S (S m)) (S O) *)
  elim (lt_irrefl (S n0) H0).
Qed.

Lemma mult_lemma5 : forall (n m:nat),((n * m) =1)->(n=1)/\(m=1).
(* Goal: @eq nat O (S O) *)
(* Goal: @eq nat (S m) (S O) *)
  induction n;simpl;intros;try discriminate.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat m (S O)) *)
  induction m.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat O (S O)) *)
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  rewrite mult_comm in H.
(* Goal: @eq nat O (S O) *)
(* Goal: @eq nat (S m) (S O) *)
  simpl in H;discriminate.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  assert ((S n)<=((S n)*(S m))).
(* Goal: @eq nat O (S O) *)
(* Goal: @eq nat (S m) (S O) *)
  apply mult_lemma1;discriminate.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  assert (((S n)*(S m))=((S m)+n*(S m))).
(* Goal: @eq nat (Init.Nat.mul (S n) (S m)) (Init.Nat.add (S m) (Init.Nat.mul n (S m))) *)
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  reflexivity.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  rewrite H1 in H0.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  rewrite H in H0.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  assert ((S n)=1).
(* Goal: lt O (Init.Nat.sub b a) *)
  omega.
(* Goal: and (@eq nat (S n) (S O)) (@eq nat (S m) (S O)) *)
  split;trivial.
(* Goal: @eq nat (S m) (S O) *)
  inversion H2.
(* Goal: @eq nat (S m) (S O) *)
  rewrite H4 in H.
(* Goal: @eq nat (S m) (S O) *)
  simpl in H.
(* Goal: lt O (Init.Nat.sub b a) *)
  omega.
Qed.

Lemma plus_minus_lemma1 : forall (y x:nat),(x+y-y=x).
(* Goal: @eq nat (Init.Nat.mul a n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  induction y;intros;rewrite plus_comm;simpl.
(* Goal: @eq nat (Init.Nat.sub x O) x *)
(* Goal: @eq nat (Init.Nat.sub (Nat.add y x) y) x *)
  auto with arith.
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.add n (Init.Nat.mul a n)) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite plus_comm.
(* Goal: @eq nat (Init.Nat.sub (Nat.add x y) y) x *)
  apply IHy.
Qed.

Lemma mult_minus_lemma1 : forall (a n:nat),a*n-n = (a-1)*n.
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: forall (a b n : nat) (_ : not (@eq nat n O)) (_ : @eq nat (Init.Nat.mul n a) (Init.Nat.mul n b)), @eq nat a b *)
  induction a.
(* Goal: @eq nat (Init.Nat.mul a n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  simpl.
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  trivial.
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  replace (S a*n) with (n+a*n);try (auto with arith).
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.add n (Init.Nat.mul a n)) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite plus_comm.
(* Goal: @eq nat (Init.Nat.sub (Nat.add (Init.Nat.mul a n) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite plus_minus_lemma1.
(* Goal: @eq nat (Init.Nat.mul a n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  simpl.
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite <- minus_n_O;trivial.
Qed.

Lemma mult_lemma6 : forall (a b n:nat),(n <> O)->(n*a=n*b)->(a=b).
(* Goal: forall (a b n : nat) (_ : not (@eq nat n O)) (_ : @eq nat (Init.Nat.mul n a) (Init.Nat.mul n b)), @eq nat a b *)
  induction a.
(* Goal: forall (b n : nat) (_ : not (@eq nat n O)) (_ : @eq nat (Init.Nat.mul n O) (Init.Nat.mul n b)), @eq nat O b *)
(* Goal: forall (b n : nat) (_ : not (@eq nat n O)) (_ : @eq nat (Init.Nat.mul n (S a)) (Init.Nat.mul n b)), @eq nat (S a) b *)
  intros;rewrite <- mult_n_O in H0; generalize (mult_lemma2 n b); intros Hl2; elim Hl2; intros; (auto || elim H ; auto).
(* Goal: forall (b n : nat) (_ : not (@eq nat n O)) (_ : @eq nat (Init.Nat.mul n (S a)) (Init.Nat.mul n b)), @eq nat (S a) b *)
  intros b n H.
(* Goal: forall _ : @eq nat (Init.Nat.mul n (S a)) (Init.Nat.mul n b), @eq nat (S a) b *)
  rewrite mult_comm;simpl;rewrite mult_comm;intro.
(* Goal: @eq nat (S a) b *)
  assert (n*a = n*b-n).
(* Goal: @eq nat (Init.Nat.mul n a) (Init.Nat.sub (Init.Nat.mul n b) n) *)
(* Goal: @eq nat (S a) b *)
  apply plus_minus;auto.
(* Goal: @eq nat (S a) b *)
  assert (a*n=(b-1)*n).
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite <- mult_minus_lemma1;rewrite mult_comm;rewrite (mult_comm b n);trivial.
(* Goal: @eq nat (S a) b *)
  assert (a=(b-1)).
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  apply (IHa (b-1) n);trivial.
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite mult_comm;rewrite (mult_comm n (b-1));trivial.
(* Goal: @eq nat (S a) b *)
  destruct b;simpl in H3.
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite H3 in H0;rewrite (mult_comm n 0) in H0;rewrite plus_comm in H0;simpl in H0;elim H;trivial.
(* Goal: @eq nat (S a) (S b) *)
  rewrite <- minus_n_O in H3;auto.
Qed.

Lemma mult_lemma7 : forall (x y z t:nat),x*y*(z*t)=z*(x*y*t).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul x y) (Init.Nat.mul z t)) (Init.Nat.mul z (Init.Nat.mul (Init.Nat.mul x y) t)) *)
  ring.
Qed.

Lemma minus_lemma1 : forall (a b:nat),(S a-S b)<S a.
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: lt O (Init.Nat.sub b a) *)
  omega.
Qed.

Lemma minus_lemma2 : forall (n m:nat),(n<=m)->(n-m=O).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: lt O (Init.Nat.sub b a) *)
  omega.
Qed.

Lemma mult_minus_lemma2 : forall (x y z:nat),(x*(y-z))=(x*y-x*z).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: @eq nat (Init.Nat.mul x (Init.Nat.sub y z)) (Init.Nat.sub (Init.Nat.mul x y) (Init.Nat.mul x z)) *)
  case (le_lt_dec y z);intro.
(* Goal: @eq nat (Init.Nat.sub x O) x *)
(* Goal: @eq nat (Init.Nat.sub (Nat.add y x) y) x *)
  rewrite (minus_lemma2 y z l);rewrite mult_comm;simpl;rewrite minus_lemma2;trivial;auto with arith.
(* Goal: @eq nat (Init.Nat.mul x (Init.Nat.sub y z)) (Init.Nat.sub (Init.Nat.mul x y) (Init.Nat.mul x z)) *)
  assert (y=z+(y-z)).
(* Goal: @eq nat y (Init.Nat.add z (Init.Nat.sub y z)) *)
(* Goal: @eq nat (Init.Nat.mul x (Init.Nat.sub y z)) (Init.Nat.sub (Init.Nat.mul x y) (Init.Nat.mul x z)) *)
  rewrite <- (le_plus_minus z y);try (auto with arith).
(* Goal: @eq nat (Init.Nat.mul x (Init.Nat.sub y z)) (Init.Nat.sub (Init.Nat.mul x y) (Init.Nat.mul x z)) *)
  replace (x*y) with (x*(z+(y-z))).
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite mult_plus_distr_l;rewrite minus_plus;trivial.
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite <- H;trivial.
Qed.

Lemma plus_minus_lemma2 : forall (x y z:nat),(y<=x)->(x-y+z)=(x+z-y).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.sub x y) z) (Init.Nat.sub (Init.Nat.add x z) y) *)
  rewrite (le_plus_minus y x);try (auto with arith).
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite minus_plus;rewrite <- plus_assoc;rewrite minus_plus;trivial.
Qed.

Lemma minus_minus_lemma1 : forall (x y z:nat),(z<=y)->(x-(y-z))=(x+z-y).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite (le_plus_minus z y);trivial.
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  rewrite minus_plus;rewrite plus_comm;rewrite <- minus_plus_simpl_l_reverse;trivial.
Qed.

Lemma minus_minus_lemma2 : forall (x y z:nat),(x-y-z)=(x-(y+z)).
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  induction x;simpl;trivial.
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: @eq nat O O *)
(* Goal: @eq nat (Init.Nat.sub (Init.Nat.mul (S a) n) n) (Init.Nat.mul (Init.Nat.sub (S a) (S O)) n) *)
  case y;simpl;trivial.
Qed.

Lemma minus_lt_lemma1 : forall (b a:nat),(a<b)->(0<b-a).
(* Goal: forall (b a : nat) (_ : lt a b), lt O (Init.Nat.sub b a) *)
  intros.
(* Goal: lt O (Init.Nat.sub b a) *)
  omega.
Qed.
