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

(** First, we show the following theorem: *)
(** if p is a prime number and gcd(p,k)=1 then sqrt(p*k) is not rational *)

(** Then, we strengthen the result to the n-th root of p^r*k *)
(** where 0 < r < n obtaining the theorem: *)
(**  if p is a prime number, gcd(p,k)=1 and 0 < r < n then the n-th root of p^r*k is not rational *)

Require Import missing.
Require Import division.
Require Import gcd.
Require Import primes.
Require Import power.

Unset Standard Proposition Elimination Names.

(** now, we show the result claimed in the header *)
Lemma sqrt_prime_irrat_aux : forall (p k a b:nat),(is_prime p)->(rel_prime p k)->(rel_prime a b)->(p*k*(square b) <> (square a)).
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  intros.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  intro.
(* Goal: False *)
  assert (divides a p).
(* Goal: divides a p *)
(* Goal: False *)
  apply prime_square;trivial.
(* Goal: divides (square a) p *)
(* Goal: False *)
  exists (k*(square b)).
(* Goal: @eq nat (square a) (Init.Nat.mul p (Init.Nat.mul k (square b))) *)
(* Goal: False *)
  rewrite <- H2;ring.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  elim H3;intro n_a;intro.
(* Goal: False *)
  rewrite H4 in H2;rewrite square_mult_lemma in H2;unfold square in H2.
(* Goal: False *)
  assert (k*(b*b)=p*(n_a*n_a)).
(* Goal: @eq nat (Init.Nat.mul k (Init.Nat.mul b b)) (Init.Nat.mul p (Init.Nat.mul n_a n_a)) *)
(* Goal: False *)
  apply mult_lemma6 with p.
(* Goal: not (@eq nat p O) *)
(* Goal: @eq nat (Init.Nat.mul p (Init.Nat.mul k (Init.Nat.mul b b))) (Init.Nat.mul p (Init.Nat.mul p (Init.Nat.mul n_a n_a))) *)
(* Goal: False *)
  intro H5;rewrite H5 in H;apply not_prime_zero;trivial.
(* Goal: @eq nat (Init.Nat.mul p (Init.Nat.mul k (Init.Nat.mul b b))) (Init.Nat.mul p (Init.Nat.mul p (Init.Nat.mul n_a n_a))) *)
(* Goal: False *)
  rewrite mult_assoc;rewrite H2;ring.
(* Goal: False *)
  assert (divides b p).
(* Goal: divides b p *)
(* Goal: False *)
  apply prime_square;trivial;unfold square.
(* Goal: divides (Init.Nat.mul b b) p *)
(* Goal: False *)
  apply gauss with k.
(* Goal: rel_prime k p *)
(* Goal: divides (Init.Nat.mul k (Init.Nat.mul b b)) p *)
(* Goal: False *)
  apply rel_prime_sym;trivial.
(* Goal: divides (Init.Nat.mul k (Init.Nat.mul b b)) p *)
(* Goal: False *)
  exists (n_a*n_a);trivial.
(* Goal: False *)
  assert (p=1).
(* Goal: @eq nat p (S O) *)
(* Goal: False *)
  unfold rel_prime in H1.
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  elim H1;intros.
(* Goal: @eq nat p (S O) *)
(* Goal: False *)
  apply divides_antisym;try (apply one_min_div).
(* Goal: divides (S O) p *)
  apply H8;red;tauto.
(* Goal: False *)
  elim H;tauto.
Qed.

(** Theorem: if p is prime, p and k are relatively prime, then sqrt(p*k) is not rationnal *)
Theorem sqrt_prime_irrat : forall (p k a b:nat),(is_prime p)->(rel_prime p k)->(b<>O)->(p*k*(square b) <> (square a)).
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  intros.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (gcd_is_gcd a b);intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (quo_is_quo a (gcd a b) (gcd_div_l (gcd a b) a b H2));intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (quo_is_quo b (gcd a b) (gcd_div_r (gcd a b) a b H2));intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  intro.
(* Goal: False *)
  rewrite H3 in H5.
(* Goal: False *)
  replace (square b) with (square (gcd a b * quo b (gcd a b) (gcd_div_r (gcd a b) a b H2))) in H5;auto.
(* Goal: False *)
  rewrite square_mult_lemma in H5;rewrite square_mult_lemma in H5.
(* Goal: False *)
  assert (p*k*(square (quo b (gcd a b) (gcd_div_r (gcd a b) a b H2)))=(square (quo a (gcd a b) (gcd_div_l (gcd a b) a b H2)))).
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul p k) (square (quo b (gcd a b) (gcd_div_r (gcd a b) a b H2)))) (square (quo a (gcd a b) (gcd_div_l (gcd a b) a b H2))) *)
(* Goal: False *)
  apply mult_lemma6 with (square (gcd a b)).
(* Goal: not (@eq nat (square (gcd a b)) O) *)
(* Goal: @eq nat (Init.Nat.mul (square (gcd a b)) (Init.Nat.mul (Init.Nat.mul p k) (square (quo b (gcd a b) (gcd_div_r (gcd a b) a b H2))))) (Init.Nat.mul (square (gcd a b)) (square (quo a (gcd a b) (gcd_div_l (gcd a b) a b H2)))) *)
(* Goal: False *)
  unfold square.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (gcd_non_zero (gcd a b) a b H1 H2);intro.
(* Goal: not (@eq nat (Init.Nat.mul (gcd a b) (gcd a b)) O) *)
(* Goal: @eq nat (Init.Nat.mul (square (gcd a b)) (Init.Nat.mul (Init.Nat.mul p k) (square (quo b (gcd a b) (gcd_div_r (gcd a b) a b H2))))) (Init.Nat.mul (square (gcd a b)) (square (quo a (gcd a b) (gcd_div_l (gcd a b) a b H2)))) *)
(* Goal: False *)
  intro;apply H6.
(* Goal: @eq nat (gcd a b) O *)
(* Goal: @eq nat (Init.Nat.mul (square (gcd a b)) (Init.Nat.mul (Init.Nat.mul p k) (square (quo b (gcd a b) (gcd_div_r (gcd a b) a b H2))))) (Init.Nat.mul (square (gcd a b)) (square (quo a (gcd a b) (gcd_div_l (gcd a b) a b H2)))) *)
(* Goal: False *)
  case (mult_lemma2 (gcd a b) (gcd a b) H7);trivial.
(* Goal: @eq nat (Init.Nat.mul (square (gcd a b)) (Init.Nat.mul (Init.Nat.mul p k) (square (quo b (gcd a b) (gcd_div_r (gcd a b) a b H2))))) (Init.Nat.mul (square (gcd a b)) (square (quo a (gcd a b) (gcd_div_l (gcd a b) a b H2)))) *)
(* Goal: False *)
  rewrite <- H5;ring.
(* Goal: False *)
  apply (sqrt_prime_irrat_aux p k (quo a (gcd a b) (gcd_div_l (gcd a b) a b H2)) (quo b (gcd a b) (gcd_div_r (gcd a b) a b H2)));auto.
(* Goal: rel_prime (quo a (gcd a b) (gcd_div_l (gcd a b) a b H5)) (quo b (gcd a b) (gcd_div_r (gcd a b) a b H5)) *)
  apply gcd_rel_prime;apply (gcd_non_zero (gcd a b) a b);trivial.
Qed.

(** if p is prime then sqrt(p) is not rationnal *)
Fact sqrt_prime : forall (p:nat),(is_prime p)->forall (a b:nat),(b<>O)->(p*(square b)<>(square a)).
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  intros.
(* Goal: not (@eq nat (Init.Nat.mul p (square b)) (square a)) *)
  replace p with (p*1);try (auto with arith).
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul p (S O)) (square b)) (square a)) *)
  apply sqrt_prime_irrat;trivial;apply rel_prime_1.
Qed.

(** We now deduce from this theorem that sqrt(2) is not rationnal *)
(** here is it! *)
Fact sqrt_2_irrat : forall (p q:nat),(q<>O)->(2*(square q)<>(square p)).
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  intros.
(* Goal: not (@eq nat (Init.Nat.mul (S (S O)) (square q)) (square p)) *)
  apply sqrt_prime;trivial.
(* Goal: is_prime (S (S O)) *)
  apply is_prime_2.
Qed.

(** generalisation *)
Lemma nth_root_irrat_aux : forall (p k a b n r:nat),(is_prime p)->(rel_prime p k)->(0<r)->(r<n)->(rel_prime a b)->((power p r)*k*(power b n) <> (power a n)).
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  intros.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  intro.
(* Goal: False *)
  assert (divides a p).
(* Goal: divides b p *)
(* Goal: False *)
  apply prime_power with n;trivial.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (power_divides_lemma1 r p H1);intro.
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  elim H5;intro q;intros.
(* Goal: divides b p *)
(* Goal: False *)
  rewrite H6 in H4.
(* Goal: divides (power a n) p *)
(* Goal: False *)
  rewrite <- H4;exists (q*k*(power b n));ring.
(* Goal: False *)
  assert (divides b p).
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  elim H5;intro q;intros.
(* Goal: divides b p *)
(* Goal: False *)
  rewrite H6 in H4.
(* Goal: divides b p *)
(* Goal: False *)
  rewrite power_mult_lemma1 in H4.
(* Goal: divides b p *)
(* Goal: False *)
  assert ((power p n)=(power p (r+(n-r)))).
(* Goal: @eq nat (power p n) (power p (Init.Nat.add r (Init.Nat.sub n r))) *)
(* Goal: divides b p *)
(* Goal: False *)
  rewrite <- le_plus_minus;try (auto with arith).
(* Goal: divides b p *)
(* Goal: False *)
  rewrite H7 in H4;rewrite power_plus_lemma1 in H4.
(* Goal: divides b p *)
(* Goal: False *)
  assert ((power p r)<>O).
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  intro.
(* Goal: False *)
(* Goal: divides b p *)
(* Goal: False *)
  apply not_prime_zero.
(* Goal: is_prime O *)
(* Goal: divides b p *)
(* Goal: False *)
  assert (p=O).
(* Goal: @eq nat p O *)
(* Goal: is_prime O *)
(* Goal: divides b p *)
(* Goal: False *)
  apply power_zero with r;trivial.
(* Goal: is_prime O *)
(* Goal: divides b p *)
(* Goal: False *)
  rewrite H9 in H;trivial.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  rewrite <- mult_assoc in H4;rewrite <- mult_assoc in H4;generalize (mult_lemma6 (k*(power b n)) ((power p (n-r))*(power q n)) (power p r) H8 H4);intro.
(* Goal: divides b p *)
(* Goal: False *)
  assert (divides (power p (n-r)) p).
(* Goal: divides (power p (Init.Nat.sub n r)) p *)
(* Goal: divides b p *)
(* Goal: False *)
  apply power_divides_lemma1;apply minus_lt_lemma1;trivial.
(* Goal: divides b p *)
(* Goal: False *)
  apply prime_power with n;trivial.
(* Goal: divides (power b n) p *)
(* Goal: False *)
  apply gauss with k;try (apply rel_prime_sym;trivial).
(* Goal: divides (Init.Nat.mul k (power b n)) p *)
(* Goal: False *)
  rewrite H9;apply divides_mult;trivial.
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  elim H3;intros.
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  elim H;intros.
(* Goal: @eq nat p (S O) *)
(* Goal: False *)
  apply H9;apply divides_antisym;try (apply one_min_div).
(* Goal: divides (S O) p *)
  apply H8;red;tauto.
Qed.

(** generalization of the theorem: if p is a prime number, 0 < r < n and gcd(p,k)=1 then the n-th root of p^r*k is not rationnal! *)
Theorem nth_root_irrat : forall (p k a b n r:nat),(is_prime p)->(rel_prime p k)->(0<r)->(r<n)->(b<>0)->((power p r)*k*(power b n) <> (power a n)).
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  intros.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (gcd_is_gcd a b);intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (quo_is_quo a (gcd a b) (gcd_div_l (gcd a b) a b H5));intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (quo_is_quo b (gcd a b) (gcd_div_r (gcd a b) a b H5));intro.
(* Goal: False *)
  assert ((power a n)=(power (gcd a b * quo a (gcd a b) (gcd_div_l (gcd a b) a b H5)) n));try (rewrite <- H6;trivial).
(* Goal: False *)
  assert ((power b n)=(power (gcd a b * quo b (gcd a b) (gcd_div_r (gcd a b) a b H5)) n));try (rewrite <- H7;trivial).
(* Goal: False *)
  rewrite power_mult_lemma1 in H8;rewrite H8 in H4.
(* Goal: False *)
  rewrite power_mult_lemma1 in H9;rewrite H9 in H4.
(* Goal: False *)
  rewrite mult_lemma7 in H4.
(* Goal: False *)
  assert ((power (gcd a b) n)<>O).
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  generalize (power_zero n (gcd a b) H10);intro.
(* Goal: False *)
(* Goal: False *)
  apply (gcd_non_zero (gcd a b) a b);trivial.
(* Goal: False *)
  generalize (mult_lemma6 (power p r * k * power (quo b (gcd a b) (gcd_div_r (gcd a b) a b H5)) n) (power (quo a (gcd a b) (gcd_div_l (gcd a b) a b H5)) n) (power (gcd a b) n) H10 H4).
(* Goal: forall _ : @eq nat (Init.Nat.mul (Init.Nat.mul (power p r) k) (power (quo b (gcd a b) (gcd_div_r (gcd a b) a b H5)) n)) (power (quo a (gcd a b) (gcd_div_l (gcd a b) a b H5)) n), False *)
  fold ((power p r * k * power (quo b (gcd a b) (gcd_div_r (gcd a b) a b H5)) n)<>(power (quo a (gcd a b) (gcd_div_l (gcd a b) a b H5)) n)).
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p r) k) (power (quo b (gcd a b) (gcd_div_r (gcd a b) a b H5)) n)) (power (quo a (gcd a b) (gcd_div_l (gcd a b) a b H5)) n)) *)
  apply nth_root_irrat_aux;trivial.
(* Goal: rel_prime (quo a (gcd a b) (gcd_div_l (gcd a b) a b H5)) (quo b (gcd a b) (gcd_div_r (gcd a b) a b H5)) *)
  apply gcd_rel_prime;apply (gcd_non_zero (gcd a b) a b);trivial.
Qed.

(** Generalization of the previous theorem *)
Theorem nth_root_irrational : forall (p k a b n q r:nat),(is_prime p)->(rel_prime p k)->(0<r)->(r<n)->(b<>0)->((power p (q*n+r))*k*(power b n) <> (power a n)).
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  intros.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  intro.
(* Goal: False *)
  rewrite power_plus_lemma1 in H4.
(* Goal: False *)
  assert (divides a (power p q)).
(* Goal: divides a (power p q) *)
(* Goal: False *)
  apply prime_power_qn with n;try (auto with arith);try omega.
(* Goal: divides (power a n) (power p (Init.Nat.mul q n)) *)
(* Goal: False *)
  exists ((power p r)*k*(power b n)).
(* Goal: @eq nat (power a n) (Init.Nat.mul (power p (Init.Nat.mul q n)) (Init.Nat.mul (Init.Nat.mul (power p r) k) (power b n))) *)
(* Goal: False *)
  rewrite <- H4;ring.
(* Goal: False *)
  assert (0<n);try omega.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  elim H5;intro a';intro.
(* Goal: False *)
  rewrite H7 in H4.
(* Goal: False *)
  rewrite power_mult_lemma1 in H4;rewrite power_power_lemma1 in H4.
(* Goal: False *)
  assert ((power p (q*n))<>0).
(* Goal: is_prime O *)
(* Goal: divides b p *)
(* Goal: False *)
  intro;apply not_prime_zero;generalize (power_zero (q*n) p H8);intro;rewrite H9 in H;trivial.
(* Goal: False *)
  rewrite <- (mult_assoc (power p (q*n))) in H4;rewrite <- (mult_assoc (power p (q*n))) in H4.
(* Goal: False *)
  generalize (mult_lemma6 (power p r*k*power b n) (power a' n) (power p (q*n)) H8 H4).
(* Goal: forall _ : @eq nat (Init.Nat.mul (Init.Nat.mul (power p r) k) (power b n)) (power a' n), False *)
  fold (power p r * k * power b n <> power a' n).
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p r) k) (power b n)) (power a' n)) *)
  apply nth_root_irrat;trivial.
Qed.

(** let x and n be two numbers such that n > 0, then either the n-th root of x is a natural number of it is not rationnal *)
Theorem nth_root : forall (x n:nat),(n>0)->{y:nat | x=(power y n)}+{forall (a b:nat),(b<>0)->x*(power b n)<>(power a n)}.
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  intros.
(* Goal: sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  case (is_power_m_dec x n H);intro;try tauto.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  elim s;intro p;intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  elim p0;intro q;intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  elim p1;intro r;intro.
(* Goal: not (@eq nat (Init.Nat.mul (Init.Nat.mul (power p (Init.Nat.add (Init.Nat.mul q n) r)) k) (power b n)) (power a n)) *)
  elim p2;intro k;intro.
(* Goal: forall (x n : nat) (_ : gt n O), sumor (@sig nat (fun y : nat => @eq nat x (power y n))) (forall (a b : nat) (_ : not (@eq nat b O)), not (@eq nat (Init.Nat.mul x (power b n)) (power a n))) *)
  right;intros.
(* Goal: not (@eq nat (Init.Nat.mul x (power b n)) (power a n)) *)
  assert (x=(power p (q*n+r))*k);try tauto.
(* Goal: not (@eq nat (Init.Nat.mul x (power b n)) (power a n)) *)
  rewrite H1;apply nth_root_irrational;tauto.
Qed.
