(* 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 Import missing.
Require Import division.
Require Import Wf_nat.

Unset Standard Proposition Elimination Names.

(** lemmae about divisibility *)
Lemma divides_le : forall (a b:nat),(a<>O)->(divides a b)->(b<=a).
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intros.
(* Goal: @eq nat (remainder_euclide a b H) O *)
(* Goal: divides a b *)
  elim H0;intro q;intro.
(* Goal: le b a *)
  replace b with (b*1);try ring.
(* Goal: le (Init.Nat.mul b (S O)) a *)
  rewrite H1.
(* Goal: le (Init.Nat.mul b (S O)) (Init.Nat.mul b q) *)
  apply mult_le_compat;try omega.
(* Goal: le (S O) q *)
  destruct q;omega.
Qed.

(** Euclide theorem (existence) *)
Theorem euclide : forall (a b:nat),(b<>O)->{q:nat & { r:nat | (a=b*q+r) /\ (r < b)}}.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intros.
  apply (lt_wf_rec a (fun a:nat =>{q : nat &  {r : nat | a = b * q + r /\ r < b}})).
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intros.
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  case (le_lt_dec b n);intro.
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  elim (H0 (n-b)).
(* Goal: forall (x : nat) (_ : @sig nat (fun r : nat => and (@eq nat (Init.Nat.sub n b) (Init.Nat.add (Init.Nat.mul b x) r)) (lt r b))), @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
(* Goal: lt (Init.Nat.sub n b) n *)
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  intro q;intro.
(* Goal: lt (let (r, _) := p in r) b *)
  elim p;intro r;intro.
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
(* Goal: lt (Init.Nat.sub n b) n *)
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  exists (q+1);exists r.
(* Goal: and (not (@eq nat x n)) (divides n x) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  split;try tauto.
(* Goal: @eq nat n (Init.Nat.add (Init.Nat.mul b (Init.Nat.add q (S O))) r) *)
(* Goal: lt (Init.Nat.sub n b) n *)
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  rewrite (le_plus_minus b n);trivial.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  elim p0;intros.
(* Goal: @eq nat (Init.Nat.add b (Init.Nat.sub n b)) (Init.Nat.add (Init.Nat.mul b (Init.Nat.add q (S O))) r) *)
(* Goal: lt (Init.Nat.sub n b) n *)
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  rewrite H1;ring.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  omega.
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  exists 0;exists n.
(* Goal: and (not (@eq nat x n)) (divides n x) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  split;try tauto.
(* Goal: @eq nat n (Init.Nat.add (Init.Nat.mul b O) n) *)
  ring.
Qed.

Definition quotient_euclide (a b:nat)(H:(b<>O)) := let (q,_) := (euclide a b H) in q.

Definition remainder_euclide (a b:nat)(H:(b<>O)) := let (_,e0) := (euclide a b H) in let (r,_) := e0 in r.

(** a div b where b<>0 *)
Lemma quo_rem_euclide : forall (a b:nat)(H:(b<>O)),a=b*(quotient_euclide a b H)+(remainder_euclide a b H).
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  unfold quotient_euclide;unfold remainder_euclide;intros.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  generalize (euclide a b H);intros.
(* Goal: forall (x : nat) (_ : @sig nat (fun r : nat => and (@eq nat (Init.Nat.sub n b) (Init.Nat.add (Init.Nat.mul b x) r)) (lt r b))), @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
(* Goal: lt (Init.Nat.sub n b) n *)
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  elim s;intro q;intro.
(* Goal: lt (let (r, _) := p in r) b *)
  elim p;intro r;intro.
(* Goal: lt r b *)
  tauto.
Qed.

(** a mod b where b<>0 *)
Lemma rem_euclide : forall (a b:nat)(H:(b<>O)),(remainder_euclide a b H)<b.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  unfold remainder_euclide;intros.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  generalize (euclide a b H);intros.
(* Goal: forall (x : nat) (_ : @sig nat (fun r : nat => and (@eq nat (Init.Nat.sub n b) (Init.Nat.add (Init.Nat.mul b x) r)) (lt r b))), @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
(* Goal: lt (Init.Nat.sub n b) n *)
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  elim s;intro q;intro.
(* Goal: lt (let (r, _) := p in r) b *)
  elim p;intro r;intro.
(* Goal: lt r b *)
  tauto.
Qed.

(** Euclide division is unique *)
Lemma euclide_unique : forall (a b q r q' r':nat),(b<>O)->a=b*q+r->a=b*q'+r'->r<b->r'<b->(q=q')/\(r=r').
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intros.
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  rewrite H1 in H0.
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  case (lt_eq_lt_dec q q');intro.
(* Goal: and (@eq nat q q') (@eq nat r r') *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  case s;intro.
(* Goal: and (@eq nat q q') (@eq nat r r') *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  rewrite (le_plus_minus q q') in H0;try (auto with arith).
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  rewrite mult_plus_distr_l in H0.
(* Goal: and (@eq nat q q') (@eq nat r r') *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  assert (b*(q'-q)+r' = r).
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul b (Init.Nat.sub q' q)) r') r *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  apply plus_reg_l with (b*q).
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul b q') r') (Init.Nat.add (Init.Nat.mul b q') (Init.Nat.add (Init.Nat.mul b (Init.Nat.sub q q')) r)) *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  rewrite plus_assoc;trivial.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  assert (0<(q'-q));try omega.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  assert (b<=b*(q'-q));try omega.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  case (mult_O_le b (q'-q));intro;try omega.
(* Goal: le b (Init.Nat.mul b (Init.Nat.sub q q')) *)
  rewrite mult_comm;trivial.
(* Goal: and (not (@eq nat x n)) (divides n x) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  split;try tauto.
(* Goal: @eq nat r r' *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  rewrite <- e in H0.
(* Goal: @eq nat r r' *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  symmetry;apply plus_reg_l with (b*q);trivial.
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  rewrite (le_plus_minus q' q) in H0;try (auto with arith).
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  rewrite mult_plus_distr_l in H0.
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  assert (r'=(b*(q-q')+r)).
(* Goal: @eq nat r' (Init.Nat.add (Init.Nat.mul b (Init.Nat.sub q q')) r) *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  apply plus_reg_l with (b*q').
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul b q') r') (Init.Nat.add (Init.Nat.mul b q') (Init.Nat.add (Init.Nat.mul b (Init.Nat.sub q q')) r)) *)
(* Goal: and (@eq nat q q') (@eq nat r r') *)
  rewrite plus_assoc;trivial.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  assert (0<(q-q'));try omega.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  assert (b<=b*(q-q'));try omega.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  case (mult_O_le b (q-q'));intro;try omega.
(* Goal: le b (Init.Nat.mul b (Init.Nat.sub q q')) *)
  rewrite mult_comm;trivial.
Qed.

(** if b<>0, then b | a iff a mod b = 0 *) 
Lemma divides_euclide : forall (a b:nat)(H:(b<>O)),((divides a b)<->((remainder_euclide a b H)=O)).
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intros.
(* Goal: iff (divides a b) (@eq nat (remainder_euclide a b H) O) *)
  red.
(* Goal: and (forall _ : divides a b, @eq nat (remainder_euclide a b H) O) (forall _ : @eq nat (remainder_euclide a b H) O, divides a b) *)
  split;intro.
(* Goal: @eq nat (remainder_euclide a b H) O *)
(* Goal: divides a b *)
  generalize (quo_rem_euclide a b H);intro.
(* Goal: @eq nat (remainder_euclide a b H) O *)
(* Goal: divides a b *)
  generalize (rem_euclide a b H);intro.
(* Goal: @eq nat (remainder_euclide a b H) O *)
(* Goal: divides a b *)
  elim H0;intro q;intro.
(* Goal: @eq nat (remainder_euclide a b H) O *)
(* Goal: divides a b *)
  assert (a=b*q+0).
(* Goal: @eq nat a (Init.Nat.add (Init.Nat.mul b q) O) *)
(* Goal: @eq nat (remainder_euclide a b H) O *)
(* Goal: divides a b *)
  rewrite plus_comm;simpl;trivial.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  assert (0<b);try omega.
(* Goal: @eq nat (remainder_euclide a b H) O *)
(* Goal: divides a b *)
  generalize (euclide_unique a b (quotient_euclide a b H) (remainder_euclide a b H) q 0 H H1 H4 H2 H5).
(* Goal: lt r b *)
  intros;tauto.
(* Goal: divides a b *)
  generalize (quo_rem_euclide a b H).
(* Goal: forall _ : @eq nat a (Init.Nat.add (Init.Nat.mul b (quotient_euclide a b H)) (remainder_euclide a b H)), divides a b *)
  rewrite H0;rewrite plus_comm;simpl.
(* Goal: forall _ : @eq nat a (Init.Nat.mul b (quotient_euclide a b H)), divides a b *)
  intro;exists (quotient_euclide a b H);trivial.
Qed.

(** divisibility is decidable *)
Lemma divides_dec : forall (a b:nat),{divides a b}+{~(divides a b)}.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intros.
(* Goal: sumbool (divides a b) (not (divides a b)) *)
  case (eq_nat_dec b 0).
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  case (eq_nat_dec a 0);intros.
(* Goal: sumbool (divides a b) (not (divides a b)) *)
(* Goal: sumbool (divides a b) (not (divides a b)) *)
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  rewrite e;left;apply zero_max_div.
(* Goal: sumbool (divides a b) (not (divides a b)) *)
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  right;rewrite e;intro.
(* Goal: forall (x : nat) (_ : @sig nat (fun r : nat => and (@eq nat (Init.Nat.sub n b) (Init.Nat.add (Init.Nat.mul b x) r)) (lt r b))), @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
(* Goal: lt (Init.Nat.sub n b) n *)
(* Goal: @sigT nat (fun q : nat => @sig nat (fun r : nat => and (@eq nat n (Init.Nat.add (Init.Nat.mul b q) r)) (lt r b))) *)
  elim H;intro q;intro.
(* Goal: False *)
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  simpl in H0;apply n;trivial.
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  intro.
(* Goal: sumbool (divides a b) (not (divides a b)) *)
  case (eq_nat_dec (remainder_euclide a b n) 0);[left | right];intros;elim (divides_euclide a b n);auto.
Qed.

(** if a property about integer is decidable then it is decidable if there is an integer less than n that satisfies this property *)
Lemma dec_impl_lt_dec : forall (P:nat->Prop),(forall (n:nat),{(P n)}+{~(P n)})->(forall (m:nat),{n:nat | (n<m)/\(P(n))}+{(forall (n:nat),(n<m)->~(P n))}).
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intros.
(* Goal: sumor (@sig nat (fun n : nat => and (lt n m) (P n))) (forall (n : nat) (_ : lt n m), not (P n)) *)
  induction m.
(* Goal: sumor (@sig nat (fun n : nat => and (lt n O) (P n))) (forall (n : nat) (_ : lt n O), not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (lt n (S m)) (P n))) (forall (n : nat) (_ : lt n (S m)), not (P n)) *)
  right;intros;inversion H0.
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  case (H m);intro.
(* Goal: sumor (@sig nat (fun n : nat => and (lt n (S m)) (P n))) (forall (n : nat) (_ : lt n (S m)), not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (lt n (S m)) (P n))) (forall (n : nat) (_ : lt n (S m)), not (P n)) *)
  left;exists m;split;try (auto with arith).
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  case IHm;intro.
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  elim s;intro n0;intro.
(* Goal: sumor (@sig nat (fun n : nat => and (lt n (S m)) (P n))) (forall (n : nat) (_ : lt n (S m)), not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (lt n (S m)) (P n))) (forall (n : nat) (_ : lt n (S m)), not (P n)) *)
  left;exists n0;split;[omega | tauto].
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  right;intros.
(* Goal: not (P n1) *)
  inversion H0;trivial.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  apply n0;omega.
Qed.

(** forall n, either forall p, p<>1 /\ p<>n -> not(p | n) or there is p such that p<>1 and p<>n and p | n *) 
Lemma divides_nat : forall (n:nat),{p:nat | (p<>1)/\(p<>n)/\(divides n p)}+{forall (p:nat),(p<>1)->(p<>n)->~(divides n p)}.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intros.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  case (dec_impl_lt_dec (fun p => (p<>1)/\(divides n p))) with n;intros.
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  case (divides_dec n n0);intro.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  case (eq_nat_dec n0 1);intros.
(* Goal: lt r b *)
  right;intro;tauto.
(* Goal: lt r b *)
  left;tauto.
(* Goal: lt r b *)
  right;tauto.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  elim s;intros.
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  left;exists x.
(* Goal: and (not (@eq nat x n)) (divides n x) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  split;try tauto.
(* Goal: and (not (@eq nat x n)) (divides n x) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  split;try tauto.
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  omega.
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  case (eq_nat_dec n 0);intro.
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  rewrite e;left;exists 2.
(* Goal: and (not (@eq nat (S (S O)) O)) (divides O (S (S O))) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  split;try (intro;discriminate).
(* Goal: and (not (@eq nat (S (S O)) O)) (divides O (S (S O))) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  split;try (intro;discriminate).
(* Goal: divides O (S (S O)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  apply zero_max_div.
(* Goal: forall n : nat, sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  right;intros.
(* Goal: forall _ : not (@eq nat b O), sumbool (divides a b) (not (divides a b)) *)
  case (lt_eq_lt_dec p n);intro.
(* Goal: not (divides n p) *)
(* Goal: not (divides n p) *)
  case s;intro;[red in n0;intro;apply n0 with p;tauto | auto].
(* Goal: not (@eq nat x n) *)
(* Goal: sumor (@sig nat (fun p : nat => and (not (@eq nat p (S O))) (and (not (@eq nat p n)) (divides n p)))) (forall (p : nat) (_ : not (@eq nat p (S O))) (_ : not (@eq nat p n)), not (divides n p)) *)
  intro;generalize (divides_le n p n1 H1);omega.
Qed.
