(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** ** Exponentiation is Diophantine *)

Require Import Arith Omega Eqdep_dec ZArith.

Require Import utils_tac gcd sums Zp alpha.

Set Implicit Arguments.

Local Notation expo := (mscal mult 1).

Section expo_diophantine.

  Variables (p q r : nat).

  Definition expo_conditions :=       
      r = 0 /\ p = 1
   \/ q = 0 /\ 0 < r /\ p = 0
   \/ (0 < r /\ q <> 0) /\ exists b m a1 a2 a3, 
             (3 < q+4 /\ a1 = alpha_nat (q+4) (1+r)) 
          /\ (3 < b   /\ a2 = alpha_nat b r)
          /\ (3 < b   /\ a3 = alpha_nat b (1+r))
          /\ b = a1+q*q+2
          /\ m + q*q + 1 = b*q
          /\ p < m
          /\ rem (p+b*a2) m = rem (q*a2+a3) m.

  Let H_q3_q : 0 < q -> q*q+2 <= q*q*q+2*q.
  Proof.
(* Goal: forall _ : @eq nat p (@mscal nat Init.Nat.mul (S O) r q), expo_conditions *)
    intros H. 
(* Goal: le (Init.Nat.add (Init.Nat.mul a1 (S O)) (S O)) (Nat.add (Nat.mul a1 q) (Nat.sub (Nat.add (Nat.mul (Init.Nat.mul q q) q) (Nat.mul (S (S O)) q)) (Nat.add (Init.Nat.mul q q) (S O)))) *)
    apply plus_le_compat; try omega.
(* Goal: le (Init.Nat.mul q q) (Init.Nat.mul (Init.Nat.mul q q) q) *)
    replace q with (1+(q-1)) at 3 by omega.
(* Goal: le (Init.Nat.mul q q) (Init.Nat.mul (Init.Nat.mul (Init.Nat.add (S O) (Init.Nat.sub q (S O))) q) q) *)
    rewrite <- mult_assoc, Nat.mul_add_distr_r, Nat.mul_1_l.
(* Goal: le (Init.Nat.mul q q) (Nat.add (Nat.mul q q) (Nat.mul (Init.Nat.sub q (S O)) (Nat.mul q q))) *)
    apply le_plus_l.
  Qed.

  Lemma expo_sufficiency : p = expo r q -> expo_conditions.
  Proof.
(* Goal: forall _ : @eq nat p (@mscal nat Init.Nat.mul (S O) r q), expo_conditions *)
    intros H.
(* Goal: expo_conditions *)
    destruct (le_lt_dec r 0) as [ Hr | Hr ]; red.
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    1: { left; revert H; replace r with 0 by omega; rewrite mscal_0; tauto. } 
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    destruct (eq_nat_dec q 0) as [ Hq | Hq ].
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    1: { right; left; subst; rewrite power_of_0; auto. }
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    remember (alpha_nat (q+4) (S r)) as a1.
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    remember (a1+q*q+2) as b.
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    remember (alpha_nat b r) as a2.
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    remember (alpha_nat b (1+r)) as a3.
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    remember (b*q-q*q-1) as m.
(* Goal: or (and (@eq nat r O) (@eq nat p (S O))) (or (and (@eq nat q O) (and (lt O r) (@eq nat p O))) (and (and (lt O r) (not (@eq nat q O))) (@ex nat (fun b : nat => @ex nat (fun m : nat => @ex nat (fun a1 : nat => @ex nat (fun a2 : nat => @ex nat (fun a3 : nat => and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))))))))))) *)
    right; right; split; auto; exists b, m, a1, a2, a3.
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
    assert (3 < b) as Hb.
(* Goal: lt (@mscal nat Init.Nat.mul (S O) r q) m *)
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
    { rewrite Heqb.
(* Goal: lt (S (S (S O))) (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O))) *)
      apply lt_le_trans with (1+(1*1)+2); try omega.
(* Goal: le (Init.Nat.add (Init.Nat.add (S O) (Init.Nat.mul (S O) (S O))) (S (S O))) (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O))) *)
      repeat apply plus_le_compat; auto.
      + rewrite Heqa1.
(* Goal: le (S O) (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (S r)) *)
        apply alpha_nat_mono with (i := 1); omega.
      + apply mult_le_compat; omega. }
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
    assert (2 <= b) as Hb' by omega.
    destruct (@alpha_nat_power (q+4)) with (n := r)
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
        as (H1 & H2); try omega.
    assert (q*q+2 <= q*q*q+2*q) as Hq'.
    { apply H_q3_q; omega. }
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
    assert (m <> 0) as Hm.
(* Goal: lt (@mscal nat Init.Nat.mul (S O) r q) m *)
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
    { rewrite Heqm, Heqb.
      do 2 rewrite  Nat.mul_add_distr_r.
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add (Nat.mul a1 q) (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
      assert (a1*q <> 0) as Ha1.
(* Goal: lt (@mscal nat Init.Nat.mul (S O) r q) m *)
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
      { intros E; apply mult_is_O in E.
(* Goal: False *)
        destruct E as [ E | ]; try omega.
(* Goal: le (S O) a1 *)
        revert E; rewrite Heqa1.
        apply alpha_nat_gt_0; omega. }
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add (Nat.mul a1 q) (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
      revert Ha1; generalize (a1*q); intros x Hx.
      omega. }
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
    assert (expo r q < m) as Hexpo.
(* Goal: lt (@mscal nat Init.Nat.mul (S O) r q) m *)
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
    { rewrite Heqm, Heqb. 
(* Goal: lt (@mscal nat Init.Nat.mul (S O) r q) (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O))) q) (Init.Nat.mul q q)) (S O)) *)
      do 2 rewrite Nat.mul_add_distr_r.
(* Goal: lt (@mscal nat Init.Nat.mul (S O) r q) (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add (Nat.mul a1 q) (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) *)
      rewrite <- Heqa1 in H1.
      apply lt_le_trans with (a1*1+1).
      + rewrite plus_comm, Nat.mul_1_r; apply le_n_S.
(* Goal: le (@mscal nat Init.Nat.mul (S O) r q) a1 *)
        apply le_trans with (2 := H1).
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
        apply power_mono_r; omega.
      + rewrite <- Nat.sub_add_distr, <- plus_assoc, <- Nat.add_sub_assoc; try omega.
(* Goal: le (Init.Nat.add (Init.Nat.mul a1 (S O)) (S O)) (Nat.add (Nat.mul a1 q) (Nat.sub (Nat.add (Nat.mul (Init.Nat.mul q q) q) (Nat.mul (S (S O)) q)) (Nat.add (Init.Nat.mul q q) (S O)))) *)
        apply plus_le_compat; try omega.
        apply mult_le_compat; omega. }  
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
    repeat (split; auto); try omega.
(* Goal: @eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m) *)
    rewrite <- nat2Zp_inj with (Hp := Hm).
(* Goal: @eq (Z_Zp m) (@nat2Zp m Hm (Init.Nat.add p (Init.Nat.mul b a2))) (@nat2Zp m Hm (Init.Nat.add (Init.Nat.mul q a2) a3)) *)
    do 2 rewrite nat2Zp_plus.
(* Goal: @eq (Z_Zp m) (@Zp_plus m Hm (@nat2Zp m Hm p) (@nat2Zp m Hm (Init.Nat.mul b a2))) (@Zp_plus m Hm (@nat2Zp m Hm (Init.Nat.mul q a2)) (@nat2Zp m Hm a3)) *)
    rewrite Heqa2. 
(* Goal: @eq (Z_Zp m) (@Zp_plus m Hm (@nat2Zp m Hm p) (@nat2Zp m Hm (Init.Nat.mul b (alpha_nat b r)))) (@Zp_plus m Hm (@nat2Zp m Hm (Init.Nat.mul q (alpha_nat b r))) (@nat2Zp m Hm a3)) *)
    revert Hm; rewrite Heqm; intros Hm.
(* Goal: @eq (Z_Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O))) (@Zp_plus (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm p) (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (Init.Nat.mul b (alpha_nat b r)))) (@Zp_plus (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (Init.Nat.mul q (alpha_nat b r))) (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm a3)) *)
    rewrite expo_congruence; auto.
(* Goal: @eq (Z_Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O))) (@Zp_plus (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm p) (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (Init.Nat.mul b (alpha_nat b r)))) (@Zp_plus (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (Init.Nat.add (alpha_nat b (Init.Nat.sub r (S O))) (@mscal nat Init.Nat.mul (S O) r q))) (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm a3)) *)
    rewrite <- H, plus_comm, nat2Zp_plus, <- Zp_plus_assoc; f_equal.
(* Goal: @eq (Z_Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O))) (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (Init.Nat.mul b (alpha_nat b r))) (@Zp_plus (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm (alpha_nat b (Init.Nat.sub r (S O)))) (@nat2Zp (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul b q) (Init.Nat.mul q q)) (S O)) Hm a3)) *)
    rewrite <- nat2Zp_plus; f_equal.
(* Goal: @eq nat (Init.Nat.mul b (alpha_nat b r)) (Init.Nat.add (alpha_nat b (Init.Nat.sub r (S O))) a3) *)
    rewrite Heqa3.
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
    destruct r as [ | r' ]; try omega.
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
    replace (S r' -1) with r' by omega.
(* Goal: @eq nat (Init.Nat.mul b (alpha_nat b (S r'))) (Init.Nat.add (alpha_nat b r') (alpha_nat b (Init.Nat.add (S O) (S r')))) *)
    simpl plus at 2.
(* Goal: @eq nat (Init.Nat.mul b (alpha_nat b (S r'))) (Init.Nat.add (alpha_nat b r') (alpha_nat b (S (S r')))) *)
    rewrite alpha_nat_fix_2.
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
    generalize (alpha_nat_le Hb' r'); omega.
  Qed.

  Infix "⊕" := (Zp_plus _) (at level 50, left associativity).
  Infix "⊗" := (Zp_mult _) (at level 40, left associativity).
  Notation "∸" := (Zp_opp _).
  Notation f := (nat2Zp _).
  Notation "〚 x 〛" :=  (f x).

  Ltac fold_nat2Zp := 
    repeat match goal with 
      | |- context[nat2Zp _ ?x ⊕ nat2Zp _ ?y] => rewrite <- nat2Zp_plus
      | |- context[nat2Zp _ ?x ⊗ nat2Zp _ ?y] => rewrite <- nat2Zp_mult
      | |- context[∸ nat2Zp _ ?x] => fail
    end.

  Lemma expo_necessity : expo_conditions -> p = expo r q.
  Proof.
    unfold expo_conditions.
    intros [ (H1 & H2) | [ (H1 & H2 & H3) | ((H0 & H1) & b & m & a1 & a2 & a3 & (_ & H2) & 
                                            (H3 & H4) & (H5 & H6) & H7 & H8 & H9 & H10) ] ].
    + subst; auto.    
    + subst; rewrite power_of_0; auto.
    + assert (m = b*q - q*q -1) as Hm1 by omega.
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
      assert (m <> 0) as Hm by omega.
      assert (q*q+2 <= q*q*q+2*q) as Hq'.
      { apply H_q3_q; omega. }
      assert (expo r q < m) as Hq.
(* Goal: lt (@mscal nat Init.Nat.mul (S O) r q) m *)
(* Goal: and (and (lt (S (S (S O))) (Init.Nat.add q (S (S (S (S O)))))) (@eq nat a1 (alpha_nat (Init.Nat.add q (S (S (S (S O))))) (Init.Nat.add (S O) r)))) (and (and (lt (S (S (S O))) b) (@eq nat a2 (alpha_nat b r))) (and (and (lt (S (S (S O))) b) (@eq nat a3 (alpha_nat b (Init.Nat.add (S O) r)))) (and (@eq nat b (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O)))) (and (@eq nat (Init.Nat.add (Init.Nat.add m (Init.Nat.mul q q)) (S O)) (Init.Nat.mul b q)) (and (lt p m) (@eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m))))))) *)
      { rewrite Hm1, H7.
(* Goal: lt (@mscal nat Init.Nat.mul (S O) r q) (Init.Nat.sub (Init.Nat.sub (Init.Nat.mul (Init.Nat.add (Init.Nat.add a1 (Init.Nat.mul q q)) (S (S O))) q) (Init.Nat.mul q q)) (S O)) *)
        do 2 rewrite Nat.mul_add_distr_r.
        apply lt_le_trans with (a1*1+1).
        + rewrite plus_comm, Nat.mul_1_r; apply le_n_S.
          destruct alpha_nat_power with (b_nat := q+4) (n := r)
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
            as (G1 & _); try omega.
          rewrite H2. 
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
          apply le_trans with (2 := G1), power_mono_r; omega.
        + rewrite <- Nat.sub_add_distr, <- plus_assoc, <- Nat.add_sub_assoc; try omega.
(* Goal: le (Init.Nat.add (Init.Nat.mul a1 (S O)) (S O)) (Nat.add (Nat.mul a1 q) (Nat.sub (Nat.add (Nat.mul (Init.Nat.mul q q) q) (Nat.mul (S (S O)) q)) (Nat.add (Init.Nat.mul q q) (S O)))) *)
          apply plus_le_compat; try omega.
          apply mult_le_compat; omega. }
      rewrite <- (rem_lt Hm H9), <- (rem_lt Hm Hq).
      revert H10. 
      rewrite Hm1 in Hm |- *.
(* Goal: @eq nat (rem (Init.Nat.add p (Init.Nat.mul b a2)) m) (rem (Init.Nat.add (Init.Nat.mul q a2) a3) m) *)
      do 2 rewrite <- nat2Zp_inj with (Hp := Hm).
(* Goal: @eq (Z_Zp m) (@nat2Zp m Hm (Init.Nat.add p (Init.Nat.mul b a2))) (@nat2Zp m Hm (Init.Nat.add (Init.Nat.mul q a2) a3)) *)
      do 2 rewrite nat2Zp_plus.
      rewrite H4, expo_congruence; auto; [ | omega ].
      rewrite H6, nat2Zp_plus.
      destruct r as [ | r' ]; [ omega | ].
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
      replace (S r' -1) with r' by omega.
      simpl plus.
      rewrite alpha_nat_fix_2, nat2Zp_minus. 
(* Goal: not (@eq nat (Init.Nat.sub (Init.Nat.sub (Nat.add (Nat.add x (Nat.mul (Init.Nat.mul q q) q)) (Nat.mul (S (S O)) q)) (Init.Nat.mul q q)) (S O)) O) *)
      2: apply alpha_nat_le; omega.
      intros H; rewrite Zp_opp_plus_eq in H.
      rewrite H.
      rewrite (Zp_plus_comm _ 〚b * _〛 (∸ _)).
      repeat rewrite <- Zp_plus_assoc.
      rewrite Zp_minus, Zp_plus_zero_r.
      rewrite Zp_plus_comm, <- Zp_plus_assoc.
      rewrite (Zp_plus_comm _ (∸ _)), Zp_minus, Zp_plus_zero_r.
      trivial.
  Qed.

End expo_diophantine.

Local Hint Resolve expo_sufficiency expo_necessity.

Theorem expo_diophantine p q r : p = expo r q <-> expo_conditions p q r.
Proof. split; auto. Qed.
