(* 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 euclide.
Require Import gcd.
Require Import power.
Require Import permutation.
Require Import Wf_nat.

Unset Standard Proposition Elimination Names.

(** definition of a "prime number" *)
Definition is_prime (p:nat) := (p<>1)/\(forall (d:nat),(divides p d)->(d=1)\/(d=p)).

Lemma not_prime_zero : ~(is_prime O).
(* Goal: forall (d p a : nat) (_ : is_prime p) (_ : is_gcd d a p), or (@eq nat d (S O)) (@eq nat d p) *)
  unfold is_prime.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: False *)
  case (H1 2);try (apply zero_max_div);intro;discriminate.
Qed.

(** 2 is a prime number *)
Lemma is_prime_2 : (is_prime 2).
(* Goal: forall (d p a : nat) (_ : is_prime p) (_ : is_gcd d a p), or (@eq nat d (S O)) (@eq nat d p) *)
  unfold is_prime.
(* Goal: and (@eq nat n (Init.Nat.mul (power p m) (quo n (power p m) H3))) (and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n)) *)
(* Goal: not (@eq nat n O) *)
  split.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.mul O d), or (@eq nat d (S O)) (@eq nat d (S (S O))) *)
(* Goal: forall _ : @eq nat (S (S O)) (Nat.mul (S x) d), or (@eq nat d (S O)) (@eq nat d (S (S O))) *)
  intro;discriminate.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: or (@eq nat d (S O)) (@eq nat d (S (S O))) *)
  elim H;destruct x;rewrite mult_comm.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.mul O d), or (@eq nat d (S O)) (@eq nat d (S (S O))) *)
(* Goal: forall _ : @eq nat (S (S O)) (Nat.mul (S x) d), or (@eq nat d (S O)) (@eq nat d (S (S O))) *)
  intro;discriminate.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  simpl.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add d (Nat.mul x d)), or (@eq nat d (S O)) (@eq nat d (S (S O))) *)
  case d.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  simpl.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.mul O d), or (@eq nat d (S O)) (@eq nat d (S (S O))) *)
(* Goal: forall _ : @eq nat (S (S O)) (Nat.mul (S x) d), or (@eq nat d (S O)) (@eq nat d (S (S O))) *)
  rewrite mult_comm;simpl;intro;discriminate.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: and (is_prime p) (gt n O) *)
  inversion H0.
(* Goal: or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  symmetry in H2.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (plus_is_one n (x*(S n)) H2);intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim a;intros.
(* Goal: or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
(* Goal: or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  left;rewrite H1;trivial.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim a;intros.
(* Goal: or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  right;rewrite H1;trivial.
Qed.

(** if p is prime and not(p | a) then a and p are relatively prime *)
Lemma prime_div_gcd : forall (p a:nat),(is_prime p)->~(divides a p)->(rel_prime p a).
(* Goal: forall (d p a : nat) (_ : is_prime p) (_ : is_gcd d a p), or (@eq nat d (S O)) (@eq nat d p) *)
  unfold is_prime.
(* Goal: forall (p a : nat) (_ : is_prime p) (_ : not (rel_prime a p)), divides a p *)
  unfold rel_prime.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: is_gcd d' d' p *)
(* Goal: or (@eq nat d' (S O)) (@eq nat d' p) *)
  unfold is_gcd;unfold is_cd.
(* Goal: and (@eq nat n (Init.Nat.mul (power p m) (quo n (power p m) H3))) (and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n)) *)
(* Goal: not (@eq nat n O) *)
  split.
(* Goal: and (divides p (S O)) (divides a (S O)) *)
(* Goal: forall (d' : nat) (_ : and (divides p d') (divides a d')), divides (S O) d' *)
  split;apply one_min_div.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H1;intros.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (H3 d' H4);intro.
(* Goal: divides (S O) d' *)
(* Goal: divides (S O) d' *)
  rewrite H6;apply divides_refl.
(* Goal: divides (S O) d' *)
  rewrite H6 in H5;tauto.
Qed.

(** We show some lemmae about prime numbers *)
(** if p is prime then gcd(a,p)=1 or gcd(a,p)=p *)
Lemma prime_gcd : forall (d p a:nat),(is_prime p)->(is_gcd d a p)->(d=1)\/(d=p).
(* Goal: forall (d p a : nat) (_ : is_prime p) (_ : is_gcd d a p), or (@eq nat d (S O)) (@eq nat d p) *)
  unfold is_prime.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: or (@eq nat d (S O)) (@eq nat d p) *)
  apply H2.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H0;intros.
(* Goal: divides a p *)
  elim H3;trivial.
Qed.

(** if p is prime and gcd(a,p)<>1 then p | a *)
Lemma prime_rel_prime : forall (p a:nat),(is_prime p)->~(rel_prime a p)->(divides a p).
(* Goal: forall (p a : nat) (_ : is_prime p) (_ : not (rel_prime a p)), divides a p *)
  unfold rel_prime.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  generalize (gcd_is_gcd a p);intros.
(* Goal: divides a p *)
  case (prime_gcd (gcd a p) p a H H1);intro;rewrite H2 in H1;try tauto.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H1;intros.
(* Goal: divides a p *)
  elim H3;trivial.
Qed.

(** if p is prime and p | a*b then p | a or p | b *)
Lemma prime_mult : forall (p a b:nat),(is_prime p)->(divides (a*b) p)->((divides a p)\/(divides b p)).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (gcd_is_gcd a p);intro.
(* Goal: or (divides a p) (divides b p) *)
  case (prime_gcd (gcd a p) p a H H1);intro;rewrite H2 in H1.
(* Goal: or (divides a p) (divides b p) *)
(* Goal: or (divides a p) (divides b p) *)
  right;apply gauss with a;trivial.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  red in H1;elim H1;intros.
(* Goal: or (divides a p) (divides b p) *)
  red in H3;tauto.
Qed.

(** corollary: if p is prime and p | a^2 then p | a *)
Lemma prime_square : forall (p a:nat),(is_prime p)->(divides (square a) p)->(divides a p).
(* Goal: forall (p a : nat) (_ : is_prime p) (_ : divides (square a) p), divides a p *)
  unfold square.
(* Goal: forall (p a : nat) (_ : is_prime p) (_ : divides (Init.Nat.mul a a) p), divides a p *)
  intros;case (prime_mult p a a H H0);trivial.
Qed.

(** generalisation to power *)
Lemma prime_power : forall (p n x:nat),(is_prime p)->(divides (power x n) p)->(divides x p).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  induction n;simpl;intros.
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: divides x p *)
(* Goal: divides x p *)
  elim H1;apply divides_antisym;trivial;apply one_min_div.
(* Goal: divides x p *)
  case (prime_mult p x (power x n) H H0);trivial.
(* Goal: forall _ : divides (power x n) p, divides x p *)
  intro;apply IHn;trivial.
Qed.

Lemma prime_power_qn : forall (p n q x:nat),(is_prime p)->(divides (power x n) (power p (q*n)))->(1<=n)->(divides x (power p q)).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  induction q;simpl;intros.
(* Goal: divides p (S O) *)
(* Goal: @ex nat (fun _ : nat => False) *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) a (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  apply one_min_div.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite power_plus_lemma1 in H0.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  assert (divides x (power p q)).
(* Goal: divides x (power p q) *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  apply IHq;trivial.
(* Goal: divides (power x n) (power p (Init.Nat.mul q n)) *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  elim H0;intros;exists ((power p n)*x0).
(* Goal: @eq nat (power x n) (Init.Nat.mul (power p (Init.Nat.mul q n)) (Init.Nat.mul (power p n) x0)) *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite H2;ring.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H2;intros.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite H3 in H0.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite power_mult_lemma1 in H0;rewrite power_power_lemma1 in H0;rewrite (mult_comm (power p n)) in H0.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H0;intros.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  assert ((power p (q*n))<>0).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: False *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  generalize (power_zero (q*n) p H5).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: False *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  apply not_prime_zero.
(* Goal: is_prime O *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite H6 in H;trivial.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite <- mult_assoc in H4.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  generalize (mult_lemma6 (power x0 n) ((power p n)*x1) (power p (q*n)) H5 H4).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  assert (exists n':nat,n=(S n')).
(* Goal: @ex nat (fun n' : nat => @eq nat n (S n')) *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  inversion H1;[exists 0 | exists m];trivial.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim H7;intro n';intro.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite H8 in H6;simpl in H6.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  assert (divides x0 p).
(* Goal: divides x0 p *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  case (prime_mult p x0 (power x0 n'));trivial.
(* Goal: divides (Init.Nat.mul x0 (power x0 n')) p *)
(* Goal: forall _ : divides (power x0 n') p, divides x0 p *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite H6.
(* Goal: divides (Init.Nat.mul (Init.Nat.mul p (power p n')) x1) p *)
(* Goal: forall _ : divides (power x0 n') p, divides x0 p *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  exists ((power p n')*x1);ring.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: divides x0 p *)
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  apply prime_power with n';trivial.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H9;intros.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite H10 in H3.
(* Goal: divides x (Init.Nat.mul p (power p q)) *)
  rewrite H3.
(* Goal: divides (Init.Nat.mul (power p q) (Init.Nat.mul p x2)) (Init.Nat.mul p (power p q)) *)
  exists x2;ring.
Qed.


(** study of prime numbers *)
Lemma divides_prime : forall (a:nat),(exists p:nat,(p<>a)/\(is_prime p)/\(divides a p)) -> ~(is_prime a).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intros;intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim H;intro p;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H1;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H3;intros.
(* Goal: False *)
  unfold is_prime in H0.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H0;intros.
(* Goal: False *)
  unfold is_prime in H4.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H4;intros.
(* Goal: False *)
  case (H7 p H5);auto.
Qed.

(** p<>1 is prime if forall n, gcd(n,p)=1 or gcd(n,p)=p *)
Lemma gcd_prime : forall (p:nat),(p<>1)->(forall (d a:nat),(is_gcd d a p)->(d=1)\/(d=p))->(is_prime p).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: and (is_prime n) (and (gt (S O) O) (and (@eq nat n (Init.Nat.mul (Init.Nat.mul n (S O)) (S O))) (and (is_gcd (S O) n (S O)) (lt (S O) n)))) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  split;try tauto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro d';intro.
(* Goal: or (@eq nat d' (S O)) (@eq nat d' p) *)
  assert (is_gcd d' d' p).
(* Goal: is_gcd d' d' p *)
(* Goal: or (@eq nat d' (S O)) (@eq nat d' p) *)
  unfold is_gcd;unfold is_cd.
(* Goal: and (and (divides d' d') (divides p d')) (forall (d'0 : nat) (_ : and (divides d' d'0) (divides p d'0)), divides d' d'0) *)
(* Goal: or (@eq nat d' (S O)) (@eq nat d' p) *)
  split;[split;[apply divides_refl | tauto] | tauto].
(* Goal: or (@eq nat d (S O)) (@eq nat d p) *)
  eapply H0;apply H2.
Qed.

(** p is prime iff forall n, n<>1 /\ n<>p -> not(a | p) *)
Lemma prime_cond : forall (p:nat),((p<>1)/\(forall (a:nat),(a<>1)->(a<>p)->~(divides p a))<->(is_prime p)).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  split;intros.
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: and (is_prime n) (and (gt (S O) O) (and (@eq nat n (Init.Nat.mul (Init.Nat.mul n (S O)) (S O))) (and (is_gcd (S O) n (S O)) (lt (S O) n)))) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  split;try tauto.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: or (@eq nat d (S O)) (@eq nat d p) *)
(* Goal: and (not (@eq nat p (S O))) (forall (a : nat) (_ : not (@eq nat a (S O))) (_ : not (@eq nat a p)), not (divides p a)) *)
  case (eq_nat_dec d 1);intro;try tauto.
(* Goal: or (@eq nat d (S O)) (@eq nat d p) *)
(* Goal: and (not (@eq nat p (S O))) (forall (a : nat) (_ : not (@eq nat a (S O))) (_ : not (@eq nat a p)), not (divides p a)) *)
  case (eq_nat_dec d p);intro;try tauto.
(* Goal: or (@eq nat d (S O)) (@eq nat d p) *)
(* Goal: and (not (@eq nat p (S O))) (forall (a : nat) (_ : not (@eq nat a (S O))) (_ : not (@eq nat a p)), not (divides p a)) *)
  elim (H1 d n n0 H2).
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: and (is_prime n) (and (gt (S O) O) (and (@eq nat n (Init.Nat.mul (Init.Nat.mul n (S O)) (S O))) (and (is_gcd (S O) n (S O)) (lt (S O) n)))) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  split;try tauto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intros;intro.
(* Goal: False *)
  elim (H1 a H4);auto.
Qed.

(** a number n is either prime or not (it is decidable) *)
Lemma prime_dec : forall (n:nat),{is_prime n}+{~(is_prime n)}.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (divides_nat n);intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim s;intros.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  right;intro.
(* Goal: False *)
(* Goal: sumbool (is_prime n) (not (is_prime n)) *)
  unfold is_prime in H.
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: False *)
(* Goal: sumbool (is_prime n) (not (is_prime n)) *)
  elim (H1 x);try tauto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (eq_nat_dec n 1);intro.
(* Goal: sumbool (is_prime n) (not (is_prime n)) *)
(* Goal: sumbool (is_prime n) (not (is_prime n)) *)
  right;unfold is_prime;tauto.
(* Goal: forall (d p a : nat) (_ : is_prime p) (_ : is_gcd d a p), or (@eq nat d (S O)) (@eq nat d p) *)
  left;unfold is_prime.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: or (@eq nat d (S O)) (@eq nat d n) *)
  case (eq_nat_dec d 1);try tauto.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  case (eq_nat_dec d n);try tauto;intros.
(* Goal: or (@eq nat d (S O)) (@eq nat d n) *)
  elim (n0 d n3 n2 H).
Qed.

(** if n is not prime then either n = 1 or there is a prime number p such that p | n *)
Lemma not_prime_impl_prime_divides : forall (n:nat),(~(is_prime n)->({p:nat | (is_prime p)/\(divides n p)}+{n=1})).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  apply (lt_wf_rec n (fun n:nat => ~(is_prime n)->({p:nat | (is_prime p)/\(divides n p)}+{n=1})));intros.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (eq_nat_dec n0 1);try tauto;intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (eq_nat_dec n0 0);intro.
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  left;exists 2.
(* Goal: and (is_prime (S (S O))) (divides n0 (S (S O))) *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  split;[apply is_prime_2 | rewrite e;apply zero_max_div].
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (divides_nat n0);intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim s;intro d;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim p;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H2;intros.
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  assert (d<n0).
(* Goal: lt d n0 *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  generalize (divides_le n0 d n2 H4);omega.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (prime_dec d);intro.
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  left;exists d;tauto.
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  elim (H d H5 n3);try tauto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim a;intro q;intro.
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  left;exists q.
(* Goal: and (is_prime n) (and (gt (S O) O) (and (@eq nat n (Init.Nat.mul (Init.Nat.mul n (S O)) (S O))) (and (is_gcd (S O) n (S O)) (lt (S O) n)))) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  split;try tauto.
(* Goal: divides n0 q *)
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  apply divides_trans with d;try tauto.
(* Goal: sumor (@sig nat (fun p : nat => and (is_prime p) (divides n0 p))) (@eq nat n0 (S O)) *)
  elim (prime_cond n0);intros;elim H0;apply H1;auto.
Qed.

(** if n<>0 and p is a prime number then there is m such that p^m | n and not(p^(m+1) | n) *)
Lemma nat_factor : forall (n p:nat),(is_prime p)->(n<>0)->{m:nat | (divides n (power p m))/\~(divides n (power p (m+1)))}.
(* Goal: forall (n p : nat) (_ : is_prime p) (_ : not (@eq nat n O)), @sig nat (fun m : nat => and (divides n (power p m)) (not (divides n (power p (Init.Nat.add m (S O)))))) *)
  intros n p H.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  apply (lt_wf_rec n (fun n:nat => n <> 0 -> {m : nat | divides n (power p m) /\ ~ divides n (power p (m + 1))}));intros.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (divides_dec n0 p);intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (quo_is_quo n0 p d);intro.
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  elim (H0 (quo n0 p d)).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intro m;intros.
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  exists (m+1).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim p0;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H3;intros.
(* Goal: and (divides n0 (power p (Init.Nat.add m (S O)))) (not (divides n0 (power p (Init.Nat.add (Init.Nat.add m (S O)) (S O))))) *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  rewrite H5 in H2;rewrite mult_assoc in H2.
(* Goal: and (divides n0 (power p (Init.Nat.add m (S O)))) (not (divides n0 (power p (Init.Nat.add (Init.Nat.add m (S O)) (S O))))) *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  rewrite plus_comm.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  split;simpl.
(* Goal: divides n0 (Init.Nat.mul p (power p m)) *)
(* Goal: not (divides n0 (Init.Nat.mul p (power p (Init.Nat.add m (S O))))) *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  exists x;trivial.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  rewrite plus_comm;simpl.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  rewrite (mult_comm p (power p m));rewrite mult_assoc;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H6;intros.
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  rewrite H2 in H7.
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  assert (p<>0).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: False *)
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  rewrite H8 in H.
(* Goal: False *)
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  apply not_prime_zero;trivial.
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  assert ((power p m)*x=(power p m)*p*x0).
(* Goal: @eq nat (Init.Nat.mul (power p m) x) (Init.Nat.mul (Init.Nat.mul (power p m) p) x0) *)
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  apply mult_lemma6 with p;trivial.
(* Goal: @eq nat (Init.Nat.mul p (Init.Nat.mul (power p m) x)) (Init.Nat.mul p (Init.Nat.mul (Init.Nat.mul (power p m) p) x0)) *)
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  rewrite mult_assoc;rewrite H7;ring.
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  rewrite <- H5 in H9;rewrite (mult_comm (power p m) p) in H9.
(* Goal: False *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  apply H4.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  rewrite plus_comm;simpl.
(* Goal: divides (quo n0 p d) (Init.Nat.mul p (power p m)) *)
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  exists x0;trivial.
(* Goal: lt (quo n0 p d) n0 *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  rewrite mult_comm in H2;rewrite H2;apply mult_lemma3.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: False *)
(* Goal: gt p (S O) *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  apply H1;rewrite H2;rewrite H3;trivial.
(* Goal: gt p (S O) *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  elim H.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: gt p (S O) *)
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  destruct p;omega.
(* Goal: not (@eq nat (quo n0 p d) O) *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  intro;apply H1.
(* Goal: @eq nat n0 O *)
(* Goal: @sig nat (fun m : nat => and (divides n0 (power p m)) (not (divides n0 (power p (Init.Nat.add m (S O)))))) *)
  rewrite H2;rewrite H3;ring.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  exists 0;simpl.
(* Goal: and (@eq nat n (Init.Nat.mul (power p m) (quo n (power p m) H3))) (and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n)) *)
(* Goal: not (@eq nat n O) *)
  split.
(* Goal: divides p (S O) *)
(* Goal: @ex nat (fun _ : nat => False) *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) a (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  apply one_min_div.
(* Goal: not (divides n0 (Init.Nat.mul p (S O))) *)
  rewrite mult_comm;simpl;rewrite plus_comm;simpl;trivial.
Qed.

(** if n>1 then there is a prime number p and two integers m and q with m>0 and q<n such that n=p^m*q and gcd(p,q)=1 *)
Lemma nat_factor_prime : forall (n:nat),(n<>0)->(n<>1)->{p:nat & {m:nat & {q:nat | (is_prime p)/\(m>0)/\(n=(power p m)*q)/\(is_gcd 1 p q)/\(q<n)}}}.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (prime_dec n);intro.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  exists n;exists 1;exists 1;simpl.
(* Goal: and (is_prime n) (and (gt (S O) O) (and (@eq nat n (Init.Nat.mul (Init.Nat.mul n (S O)) (S O))) (and (is_gcd (S O) n (S O)) (lt (S O) n)))) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  split;try tauto.
(* Goal: and (is_gcd (S O) n (S O)) (lt (S O) n) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  split;try omega.
(* Goal: and (@eq nat n (Init.Nat.mul (Init.Nat.mul n (S O)) (S O))) (and (is_gcd (S O) n (S O)) (lt (S O) n)) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  split;try ring.
(* Goal: and (is_gcd (S O) n (S O)) (lt (S O) n) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  split;try omega.
(* Goal: is_gcd (S O) n (S O) *)
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  apply gcd_sym;apply gcd_one.
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  elim (not_prime_impl_prime_divides n n0);intro;try tauto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim a;intro p;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim p0;intros.
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
  elim (nat_factor n p H1).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro m;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim p1;intros.
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun m : nat => @sig nat (fun q : nat => and (is_prime p) (and (gt m O) (and (@eq nat n (Init.Nat.mul (power p m) q)) (and (is_gcd (S O) p q) (lt q n))))))) *)
(* Goal: not (@eq nat n O) *)
  exists p;exists m;exists (quo n (power p m) H3).
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: and (@eq nat n (Init.Nat.mul (power p m) (quo n (power p m) H3))) (and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n)) *)
(* Goal: not (@eq nat n O) *)
  split.
(* Goal: lt O m *)
(* Goal: not (@eq nat n O) *)
  destruct m;try omega.
(* Goal: not (divides n0 (Init.Nat.mul p (S O))) *)
  elim H4;simpl;rewrite mult_comm;simpl;rewrite plus_comm;simpl;trivial.
(* Goal: and (@eq nat n (Init.Nat.mul (power p m) (quo n (power p m) H3))) (and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n)) *)
(* Goal: not (@eq nat n O) *)
  split.
(* Goal: @eq nat n (Init.Nat.mul (power p m) (quo n (power p m) H3)) *)
(* Goal: and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n) *)
(* Goal: not (@eq nat n O) *)
  apply (quo_is_quo n (power p m) H3).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (gcd_is_gcd p (quo n (power p m) H3));intro.
(* Goal: and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n) *)
(* Goal: not (@eq nat n O) *)
  assert ((gcd p (quo n (power p m) H3))=1).
(* Goal: @eq nat (gcd p (quo n (power p m) H3)) (S O) *)
(* Goal: and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n) *)
(* Goal: not (@eq nat n O) *)
  case (prime_gcd (gcd p (quo n (power p m) H3)) p (quo n (power p m) H3));trivial.
(* Goal: is_gcd (gcd p (quo n (power p m) H3)) (quo n (power p m) H3) p *)
(* Goal: forall _ : @eq nat (gcd p (quo n (power p m) H3)) p, @eq nat (gcd p (quo n (power p m) H3)) (S O) *)
(* Goal: and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n) *)
(* Goal: not (@eq nat n O) *)
  apply gcd_sym;trivial.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  rewrite H6 in H5;elim H5;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H7;intros.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  elim H4;rewrite plus_comm;simpl.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (quo_is_quo n (power p m) H3);intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H10;intros.
(* Goal: divides n (Init.Nat.mul p (power p m)) *)
(* Goal: and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n) *)
(* Goal: not (@eq nat n O) *)
  rewrite H12 in H11.
(* Goal: divides n (Init.Nat.mul p (power p m)) *)
(* Goal: and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n) *)
(* Goal: not (@eq nat n O) *)
  exists x;rewrite H11;ring.
(* Goal: and (is_gcd (S O) p (quo n (power p m) H3)) (lt (quo n (power p m) H3) n) *)
(* Goal: not (@eq nat n O) *)
  rewrite H6 in H5;trivial.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (quo_is_quo n (power p m) H3);intro.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: lt (quo n (power p m) H3) n *)
(* Goal: not (@eq nat n O) *)
  rewrite H7;rewrite mult_comm;apply mult_lemma3.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: False *)
(* Goal: gt (power p m) (S O) *)
(* Goal: not (@eq nat n O) *)
  apply H;rewrite H7.
(* Goal: @eq nat (Init.Nat.mul (power p m) (quo n (power p m) H3)) O *)
(* Goal: gt (power p m) (S O) *)
(* Goal: not (@eq nat n O) *)
  rewrite H8;ring.
(* Goal: gt (power p m) (S O) *)
(* Goal: not (@eq nat n O) *)
  red;apply power_lt.
(* Goal: gt p (S O) *)
(* Goal: le n m *)
  destruct p.
(* Goal: lt (S O) O *)
(* Goal: lt (S O) (S p) *)
(* Goal: lt O m *)
(* Goal: not (@eq nat n O) *)
  elim (not_prime_zero H1).
(* Goal: lt (S O) (S p) *)
(* Goal: lt O m *)
(* Goal: not (@eq nat n O) *)
  destruct p;try omega.
(* Goal: lt (S O) (S O) *)
(* Goal: lt O m *)
(* Goal: not (@eq nat n O) *)
  elim H1;tauto.
(* Goal: lt O m *)
(* Goal: not (@eq nat n O) *)
  destruct m;try omega.
(* Goal: not (divides n0 (Init.Nat.mul p (S O))) *)
  elim H4;simpl;rewrite mult_comm;simpl;rewrite plus_comm;simpl;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  trivial.
Qed.

(** this compute p1^n1*p2^n2*...*pm^nm if l = (p1,n1)::(p2,n2)::...::(pm,nm) *)
Fixpoint refactor (l:(list (nat*nat))) {struct l} : nat :=
  match l with
    nil => 1
    | (cons (p,n) tail) => (power p n)*(refactor tail)
  end.

(** a list l is well-formed (is a factorisation) if whenever (p,n) is in l then p is prime and n>0 and p is relatively prime to (refactor (l\(p,n))) and l\(p,n) is well-formed *)
Inductive is_wf : (list (nat*nat))->Prop :=
  nil_is_wf : (is_wf nil)
|cons_is_wf : forall (p n:nat)(tail:(list (nat*nat))),(is_prime p)->(n>0)->(is_wf tail)->(rel_prime p (refactor tail))->(is_wf (cons (p,n) tail)).

(** this gives an inefficient algorithm to compute a factorisation of n *)
Lemma factorisation : forall (n:nat),{l:(list (nat*nat)) | (is_wf l)/\n=(refactor l)}+{n=0}.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (eq_nat_dec n 0);intro.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  right;trivial.
(* Goal: sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n (refactor l)))) (@eq nat n O) *)
  case (eq_nat_dec n 1).
(* Goal: forall _ : @eq nat n (S O), sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n (refactor l)))) (@eq nat n O) *)
(* Goal: forall _ : not (@eq nat n (S O)), sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n (refactor l)))) (@eq nat n O) *)
  intro;left;exists (nil (A:=nat*nat)).
(* Goal: and (is_wf (@nil (prod nat nat))) (@eq nat n (refactor (@nil (prod nat nat)))) *)
(* Goal: forall _ : not (@eq nat n (S O)), sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n (refactor l)))) (@eq nat n O) *)
  split;[apply nil_is_wf | simpl;trivial].
(* Goal: forall _ : not (@eq nat n (S O)), sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n (refactor l)))) (@eq nat n O) *)
  generalize n0.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  apply (lt_wf_rec n (fun n:nat => n<>0 -> n <> 1 -> {l : list (nat * nat) | is_wf l /\ n = refactor l}+{n=0}));intros.
(* Goal: sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
  elim (nat_factor_prime n1 H0 H1).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro p;intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim p0;intro m;intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim p1;intro q;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim p2;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H3;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H5;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H7;intros.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (eq_nat_dec q 1);intro.
(* Goal: sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
(* Goal: sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
  left;exists (cons (p,m) nil);simpl;rewrite e in H6.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat p m) (@nil (prod nat nat))) *)
(* Goal: sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
  apply cons_is_wf;auto;try (apply nil_is_wf).
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  unfold rel_prime;simpl;rewrite e in H8;trivial.
(* Goal: sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
  assert (q<>0).
(* Goal: not (@eq nat q O) *)
(* Goal: sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
  intro;rewrite H10 in H6;rewrite mult_comm in H6;simpl in H6;auto.
(* Goal: sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
  elim (H q H9 H10 n2).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim a;intro l;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim p3;intros.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  left;exists (cons (p,m) l);simpl;rewrite H12 in H6;split;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat p m) l) *)
(* Goal: forall _ : @eq nat q O, sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
  apply cons_is_wf;auto.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  rewrite <- H12;unfold rel_prime;trivial.
(* Goal: forall _ : @eq nat q O, sumor (@sig (list (prod nat nat)) (fun l : list (prod nat nat) => and (is_wf l) (@eq nat n1 (refactor l)))) (@eq nat n1 O) *)
  intro;tauto.
Qed.

(** we now show that a factorisation is unique upto permutations *)
(** if (p,n) is in l then p^n | (refactor l) *)
Lemma factor_divides_refactor : forall (x:nat*nat)(l:list (nat*nat)),(In x l)->(divides (refactor l) (power (fst x) (snd x))).
(* Goal: forall (l : list (prod nat nat)) (p n : nat) (_ : @In (prod nat nat) (@pair nat nat p n) l) (_ : is_wf l), and (is_prime p) (gt n O) *)
  induction l;simpl;try tauto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case H;intro.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (let (p, n) := a in Init.Nat.mul (power p n) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (let (p0, n) := a in Init.Nat.mul (power p0 n) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  destruct a.
(* Goal: forall _ : @eq nat (S (S O)) (Nat.add O (Nat.mul x O)), or (@eq nat O (S O)) (@eq nat O (S (S O))) *)
(* Goal: forall (n : nat) (_ : @eq nat (S (S O)) (Nat.add (S n) (Nat.mul x (S n)))), or (@eq nat (S n) (S O)) (@eq nat (S n) (S (S O))) *)
  rewrite <- H0;simpl.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  exists (refactor l);trivial.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (let (p, n) := a in Init.Nat.mul (power p n) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (let (p0, n) := a in Init.Nat.mul (power p0 n) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  destruct a.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim (IHl H0);intros.
(* Goal: divides (Init.Nat.mul (power n n0) (refactor l)) (power (@fst nat nat x) (@snd nat nat x)) *)
  rewrite H1.
(* Goal: divides (Init.Nat.mul (power n n0) (Init.Nat.mul (power (@fst nat nat x) (@snd nat nat x)) x0)) (power (@fst nat nat x) (@snd nat nat x)) *)
  exists ((power n n0)*x0);ring.
Qed.

(** if p is prime and p | (refactor l) then there is n such that (p,n) is in l *)
Lemma prime_divides_refactor : forall (p:nat)(l:list (nat*nat)),(is_prime p)->(is_wf l)->(divides (refactor l) p)->(exists m:nat,(In (p,m) l)).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  induction l;simpl;intros.
(* Goal: @ex nat (fun _ : nat => False) *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) a (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  assert (p=1).
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply divides_antisym;trivial.
(* Goal: divides p (S O) *)
(* Goal: @ex nat (fun _ : nat => False) *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) a (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  apply one_min_div.
(* Goal: @ex nat (fun _ : nat => False) *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) a (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  rewrite H2 in H;elim H;tauto.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (let (p, n) := a in Init.Nat.mul (power p n) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (let (p0, n) := a in Init.Nat.mul (power p0 n) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  destruct a.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (divides_dec (power n n0) p);intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (prime_power p n0 n H d);intro.
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) (@pair nat nat n n0) (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) (@pair nat nat n n0) (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  assert (n=p).
(* Goal: and (is_prime p) (gt n O) *)
  inversion H0.
(* Goal: @eq nat n p *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) (@pair nat nat n n0) (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) (@pair nat nat n n0) (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  elim H6.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: @eq nat n p *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) (@pair nat nat n n0) (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) (@pair nat nat n n0) (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  case (H11 p H2);try tauto;try omega.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  exists n0;rewrite <- H3;left;trivial.
(* Goal: and (is_prime p) (gt n O) *)
  inversion H0.
(* Goal: @ex nat (fun m : nat => or (@eq (prod nat nat) (@pair nat nat n n0) (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
  elim (IHl H H7).
(* Goal: forall (x : nat) (_ : @In (prod nat nat) (@pair nat nat p x) l), @ex nat (fun m : nat => or (@eq (prod nat nat) (@pair nat nat n n0) (@pair nat nat p m)) (@In (prod nat nat) (@pair nat nat p m) l)) *)
(* Goal: divides (refactor l) p *)
  intros;exists x;tauto.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply gauss with (power n n0);trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply rel_prime_sym;apply prime_div_gcd;trivial.
Qed.


(** if (p,n) is in l and l is well-formed then p is prime and n>0 *)
Lemma in_wf : forall (l:list (nat*nat))(p n:nat),(In (p,n) l)->(is_wf l)->(is_prime p)/\(n>0).
(* Goal: forall (l : list (prod nat nat)) (p n : nat) (_ : @In (prod nat nat) (@pair nat nat p n) l) (_ : is_wf l), and (is_prime p) (gt n O) *)
  induction l;simpl;try tauto.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (let (p, n) := a in Init.Nat.mul (power p n) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (let (p0, n) := a in Init.Nat.mul (power p0 n) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intros;destruct a.
(* Goal: and (is_prime p) (gt n O) *)
  inversion H0.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  case (in_inv H);intros.
(* Goal: and (is_prime p) (gt n O) *)
(* Goal: and (is_prime p) (gt n O) *)
  inversion H8;rewrite <- H10;rewrite <- H11;try tauto.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply IHl;trivial.
Qed.

(** if (p,n) is in l and (q,m)::l is well-formed then gcd(p,q)=1 *)
Lemma rel_prime_wf : forall (l:list (nat*nat))(p n q m:nat),(In (p,n) l)->(is_wf ((q,m)::l))->(rel_prime p q).
(* Goal: forall (p n m : nat) (l : list (prod nat nat)) (_ : is_prime p) (_ : gt n O) (_ : is_wf l) (_ : divides (refactor l) (power p n)) (_ : @In (prod nat nat) (@pair nat nat p m) l), le n m *)
  induction l;simpl;intros;try tauto.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (let (p, n) := a in Init.Nat.mul (power p n) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (let (p0, n) := a in Init.Nat.mul (power p0 n) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  destruct a.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  inversion H0;case (in_inv H);intro.
(* Goal: rel_prime p q *)
(* Goal: rel_prime p q *)
  rewrite H8 in H7;simpl in H7.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim (in_wf ((n0,n1)::l) p n H);trivial;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim (mult_rel_prime q (power p n) (refactor l) H7);intros.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply rel_prime_sym;apply power_rel_prime with n;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply (IHl p n q m);trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply cons_is_wf;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  inversion H6;trivial.
(* Goal: rel_prime q (refactor l) *)
  simpl in H7;elim (mult_rel_prime q (power n0 n1) (refactor l) H7);auto.
Qed.

Inductive is_pwd : list (nat*nat) -> Prop :=
  nil_is_pwd : (is_pwd nil)
|cons_is_pwd : forall (p n:nat)(tail:list (nat*nat)),(is_pwd tail)->(forall (n:nat),~(In (p,n) tail))->(is_pwd ((p,n)::tail)).

(** if l is well-formed then the first projection of l is pairwise distinct (pwd) *)
Lemma wf_impl_pwd : forall (l:list (nat*nat)),(is_wf l)->(is_pwd l).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  induction l;intro.
(* Goal: is_pwd (@nil (prod nat nat)) *)
(* Goal: is_pwd (@cons (prod nat nat) a l) *)
  apply nil_is_pwd.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (let (p, n) := a in Init.Nat.mul (power p n) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (let (p0, n) := a in Init.Nat.mul (power p0 n) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  destruct a.
(* Goal: rel_prime p (power n0 n1) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  inversion H.
(* Goal: is_pwd (@cons (prod nat nat) (@pair nat nat n n0) l) *)
  apply cons_is_pwd;auto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intros;intro.
(* Goal: False *)
  assert (rel_prime n n).
(* Goal: rel_prime n n *)
(* Goal: False *)
  eapply rel_prime_wf;[apply H7 | apply H].
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (gcd_refl n);intro.
(* Goal: False *)
  unfold rel_prime in H8.
(* Goal: False *)
  assert (1=n).
(* Goal: @eq nat (S O) n *)
(* Goal: False *)
  eapply gcd_unique;eauto.
(* Goal: False *)
  rewrite <- H10 in H3;elim H3;tauto.
Qed.

(** if p is prime, n>0, l is well-formed and p^n | (refactor l) and (p,m) is in l then n<=m *)
Lemma prime_power_divides_refactor : forall (p n m:nat)(l:list (nat*nat)),(is_prime p)->(n>0)->(is_wf l)->(divides (refactor l) (power p n))->(In (p,m) l)->(n<=m).
(* Goal: forall (p n m : nat) (l : list (prod nat nat)) (_ : is_prime p) (_ : gt n O) (_ : is_wf l) (_ : divides (refactor l) (power p n)) (_ : @In (prod nat nat) (@pair nat nat p m) l), le n m *)
  induction l;simpl;intros;try tauto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case H3;intro.
(* Goal: le n m *)
(* Goal: le n m *)
  rewrite H4 in H2.
(* Goal: le n m *)
(* Goal: le n m *)
  rewrite H4 in H1;inversion H1.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (rel_prime_power p (refactor l) n (rel_prime_sym p (refactor l) H11));intro.
(* Goal: le n m *)
(* Goal: le n m *)
  rewrite mult_comm in H2.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (gauss (power p n) (refactor l) (power p m) H12 H2);intro.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply power_divides_power with p;trivial.
(* Goal: gt p (S O) *)
(* Goal: le n m *)
  destruct p.
(* Goal: gt O (S O) *)
(* Goal: gt (S p) (S O) *)
(* Goal: le n m *)
  elim (not_prime_zero H8).
(* Goal: gt (S p) (S O) *)
(* Goal: le n m *)
  elim H8;omega.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (let (p, n) := a in Init.Nat.mul (power p n) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (let (p0, n) := a in Init.Nat.mul (power p0 n) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  destruct a.
(* Goal: le n m *)
  inversion H1.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply IHl;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply gauss with (power n0 n1);trivial.
(* Goal: rel_prime (power n0 n1) (power p n) *)
  apply rel_prime_power;apply rel_prime_sym;apply rel_prime_power.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply (rel_prime_wf l p m n0 n1);trivial.
Qed.

(** if l and l' are well-formed and (refactor l)=(refactor l') then l is included in l' *)
Lemma factorisation_unique_upto_equiv_aux : forall (l l':list (nat*nat)),(is_wf l)->(is_wf l')->(refactor l)=(refactor l')->(forall (x n:nat),(In (x,n) l)->(In (x,n) l')).
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intros l l';intro;intro;intro;intros p n;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim (in_wf l p n H2 H);intros.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (factor_divides_refactor (p,n) l H2);simpl;intro.
(* Goal: @In (prod nat nat) (@pair nat nat p n) l' *)
  rewrite H1 in H5.
(* Goal: @In (prod nat nat) (@pair nat nat p n) l' *)
  assert (divides (refactor l') p).
(* Goal: divides (refactor l') p *)
(* Goal: @In (prod nat nat) (@pair nat nat p n) l' *)
  apply divides_trans with (power p n);[trivial | apply power_divides_lemma1;auto with arith].
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim (prime_divides_refactor p l' H3 H0 H6);intro m;intro.
(* Goal: @In (prod nat nat) (@pair nat nat p n) l' *)
  cut (n=m).
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  intro;rewrite H8;trivial.
(* Goal: @eq nat n m *)
  apply le_antisym.
(* Goal: le n m *)
(* Goal: le m n *)
  eapply prime_power_divides_refactor;eauto.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (factor_divides_refactor (p,m) l' H7);simpl;intro.
(* Goal: le m n *)
  rewrite <- H1 in H8.
(* Goal: le m n *)
  apply prime_power_divides_refactor with p l;auto.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  elim (in_wf l' p m);trivial.
Qed.

Lemma pwd_impl_set : forall (l:list (nat*nat)),(is_pwd l)->(is_set (nat*nat) l).
(* Goal: forall (l : list (prod nat nat)) (_ : is_pwd l), is_set (prod nat nat) l *)
  induction 1;[apply nil_is_set | apply cons_is_set;auto].
Qed.

(** if l and l' are well-formed and (refactor l)=(refactor l') then l' is a permutation of l *)
Lemma factorisation_unique_upto_perm : forall (l l':list (nat*nat)),(is_wf l)->(is_wf l')->(refactor l)=(refactor l')->(is_permutation (nat*nat) l l').
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: is_permutation (prod nat nat) l l' *)
  assert (forall (x n:nat),(In (x,n) l)->(In (x,n) l')).
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply factorisation_unique_upto_equiv_aux;trivial.
(* Goal: is_permutation (prod nat nat) l l' *)
  assert (forall (x n:nat),(In (x,n) l')->(In (x,n) l)).
(* Goal: forall (x n : nat) (_ : @In (prod nat nat) (@pair nat nat x n) l'), @In (prod nat nat) (@pair nat nat x n) l *)
(* Goal: is_permutation (prod nat nat) l l' *)
  apply factorisation_unique_upto_equiv_aux;auto.
(* Goal: is_permutation (prod nat nat) l l' *)
  apply is_set_eq_impl_permutation;intros;(try (apply pwd_impl_set;apply wf_impl_pwd;trivial));destruct x;split;auto.
Qed.

(** a list is a factorisation of n if l is well-formed and (refactor l)=n *)
Definition is_factorisation (n:nat)(l:list (nat*nat)) := (is_wf l)/\(n=(refactor l)).

(** The fondamental theorem of arithmetic *)
(** forall n<>0, there exists a factorisation l *)
Theorem factorisation_exists : forall (n:nat),n<>0->{l:list (nat*nat) | (is_factorisation n l)}.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  intros.
(* Goal: @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  case (factorisation n);intros;try tauto.
Qed.

(** if l and l' are two factorisation of n, then l' is a permutation of l *)
Theorem factorisation_unique_upto_permutation : forall (n:nat)(l l':list (nat*nat)),(is_factorisation n l)->(is_factorisation n l')->(is_permutation (nat*nat) l l').
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  unfold is_factorisation;intros.
(* Goal: is_permutation (prod nat nat) l l' *)
  elim H;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H0;intros.
(* Goal: is_permutation (prod nat nat) l l' *)
  apply factorisation_unique_upto_perm;auto;congruence.
Qed.

(** *)
Lemma wf_power_dec : forall (n:nat)(l:list (nat*nat)),(is_wf l)->(n>0)->{x:nat | (refactor l)=(power x n)}+{p:nat & {q:nat & {r:nat & {k:nat | (is_prime p)/\(0<r)/\(r<n)/\(refactor l)=(power p (q*n+r))*k/\(rel_prime p k)}}}}.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  induction l;simpl;intros.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  left;exists 1;rewrite power_one;trivial.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (let (p, n) := a in Init.Nat.mul (power p n) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (let (p0, n) := a in Init.Nat.mul (power p0 n) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  destruct a.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  assert (n<>0);try omega.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (quo_rem_euclide n1 n H1);intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (eq_nat_dec (remainder_euclide n1 n H1) 0);intro.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  rewrite e in H2;rewrite plus_comm in H2;simpl in H2.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  case IHl;intros;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  inversion H;trivial.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim s;intro y;intro.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  rewrite H2.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  left;rewrite p;rewrite (mult_comm n);rewrite <- power_power_lemma1;rewrite <- power_mult_lemma1;exists (power n0 (quotient_euclide n1 n H1)*y);trivial.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim s;intro p;intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim p0;intro q;intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim p1;intro r;intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim p2;intro k;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim p3;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H4;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H6;intros.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim H8;intros.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  right.
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k)))))))) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  exists p;exists q;exists r.
(* Goal: @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  rewrite H9;rewrite mult_comm;rewrite <- mult_assoc.
(* Goal: @sig nat (fun k0 : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) (Nat.mul k (power n0 n1))) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k0)) (rel_prime p k0))))) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  exists (k*(power n0 n1)).
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply rel_prime_mult;trivial.
(* Goal: rel_prime p (power n0 n1) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  inversion H.
(* Goal: rel_prime p (power n0 n1) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  rewrite H9 in H17.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim (mult_rel_prime n0 (power p (q*n+r)) k H17);intros.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply rel_prime_power;apply rel_prime_sym;apply power_rel_prime with (q*n+r);trivial.
(* Goal: gt (Init.Nat.add (Init.Nat.mul q n) r) O *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  rewrite plus_comm;auto with arith.
(* Goal: sum (@sig nat (fun x : nat => @eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  right.
(* Goal: @sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k)))))))) *)
  exists n0;exists (quotient_euclide n1 n H1);exists (remainder_euclide n1 n H1).
(* Goal: @sig nat (fun k : nat => and (is_prime n0) (and (lt O (remainder_euclide n1 n H1)) (and (lt (remainder_euclide n1 n H1) n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 (Init.Nat.add (Init.Nat.mul (quotient_euclide n1 n H1) n) (remainder_euclide n1 n H1))) k)) (rel_prime n0 k))))) *)
  rewrite (mult_comm (quotient_euclide n1 n H1));rewrite <- H2.
(* Goal: @sig nat (fun k : nat => and (is_prime n0) (and (lt O (remainder_euclide n1 n H1)) (and (lt (remainder_euclide n1 n H1) n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) k)) (rel_prime n0 k))))) *)
  exists (refactor l).
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim (in_wf ((n0,n1)::l) n0 n1);intros.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: lt O (remainder_euclide n1 n H1) *)
(* Goal: and (lt (remainder_euclide n1 n H1) n) (and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l))) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  destruct (remainder_euclide n1 n H1);try tauto;auto with arith.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: lt (remainder_euclide n1 n H1) n *)
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  apply rem_euclide.
(* Goal: and (@eq nat (Init.Nat.mul (power n0 n1) (refactor l)) (Init.Nat.mul (power n0 n1) (refactor l))) (rel_prime n0 (refactor l)) *)
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  split;trivial.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  inversion H;trivial.
(* Goal: @In (prod nat nat) (@pair nat nat n0 n1) (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  simpl;tauto.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  trivial.
Qed.

(** let n be a natural number and m>1 then either n=x^m or there is a prime number p and three numbers q,r and k such that n = p^(q*m+r)*k with 0<r<m and gcd(p,k)=1 *)
Lemma is_power_m_dec : forall (n m:nat),(m>0)->{x:nat | n=(power x m)}+{p:nat & {q:nat & {r:nat & {k:nat | (is_prime p)/\(0<r)/\(r<m)/\n=(power p (q*m+r))*k/\(rel_prime p k)}}}}.
(* Goal: forall (n m : nat) (_ : gt m O), sum (@sig nat (fun x : nat => @eq nat n (power x m))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r m) (and (@eq nat n (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q m) r)) k)) (rel_prime p k))))))))) *)
  intros n m;intro H.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  case (eq_nat_dec n 0);intro.
(* Goal: sum (@sig nat (fun x : nat => @eq nat n (power x m))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r m) (and (@eq nat n (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q m) r)) k)) (rel_prime p k))))))))) *)
(* Goal: sum (@sig nat (fun x : nat => @eq nat n (power x m))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r m) (and (@eq nat n (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q m) r)) k)) (rel_prime p k))))))))) *)
  left;exists 0.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  destruct m;simpl;try omega;trivial.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  generalize (factorisation_exists n n0);intro.
(* Goal: forall (n : nat) (l : list (prod nat nat)) (_ : is_wf l) (_ : gt n O), sum (@sig nat (fun x : nat => @eq nat (refactor l) (power x n))) (@sigT nat (fun p : nat => @sigT nat (fun q : nat => @sigT nat (fun r : nat => @sig nat (fun k : nat => and (is_prime p) (and (lt O r) (and (lt r n) (and (@eq nat (refactor l) (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k)) (rel_prime p k))))))))) *)
  elim H0;intro l;intro.
(* Goal: forall (n : nat) (_ : not (@eq nat n O)), @sig (list (prod nat nat)) (fun l : list (prod nat nat) => is_factorisation n l) *)
  elim p;intros.
(* Goal: is_wf (@cons (prod nat nat) (@pair nat nat n0 n1) l) *)
  rewrite H2;apply wf_power_dec;trivial.
Qed.
