(* This program 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 program 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 General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   modprime.
   Some nice lemmas about div, mult, mod, prime, and gcd. 
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import Arith.
Require Import ZArith.
Require Import Wf_nat.

Require Import lemmas.
Require Import natZ.
Require Import dec.
Require Import list.
Require Import exp.
Require Import divides.
Require Import prime.
Require Import modulo.
Require Import gcd.

Lemma prime_div_or_gcd1 :
 forall (p : nat) (a : Z),
 Prime p -> ZDivides (Z_of_nat p) a \/ gcd (Z_of_nat p) a 1.
Proof.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros. elim (zdivdec a (Z_of_nat p)).
(* Goal: or (@eq nat qi qi) (exlist nat (fun b : nat => @eq nat qi b) restqs) *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   left. assumption.
(* Goal: or (@eq nat qj qi) (exlist nat (fun b : nat => @eq nat qj b) restqs) *)
(* Goal: Divides a (multDrop qj (Cons nat qi restqs)) *)
(* Goal: lt O y *)
(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   right. unfold gcd in |- *. unfold common_div in |- *.
(* Goal: and (inlist nat qi (Cons nat qi restqs)) (Divides a (multDrop qi (Cons nat qi restqs))) *)
   split. split.
(* Goal: Divides (S O) (Z.abs_nat (Z.of_nat p)) *)
(* Goal: Divides (S O) (Z.abs_nat a) *)
(* Goal: forall (e : nat) (_ : and (Divides e (Z.abs_nat (Z.of_nat p))) (Divides e (Z.abs_nat a))), le e (S O) *)
   split with p. simpl in |- *. rewrite <- plus_n_O. apply abs_inj.
(* Goal: exlist nat (fun b : nat => @eq nat qi b) (Cons nat qi restqs) *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   split with (Zabs_nat a). simpl in |- *. apply plus_n_O.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros. elim H1. intros. rewrite abs_inj in H2.
(* Goal: le e (S O) *)
   elim (primediv1p p e).
(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro. rewrite H4. apply le_n.
(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro. rewrite H4 in H3. elim H0. apply divzdiv.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   rewrite abs_inj. assumption. assumption. assumption.
Qed.

Lemma divmultgcd :
 forall a b c : Z,
 a <> 0%Z -> ZDivides a (b * c) -> gcd a b 1 -> ZDivides a c.
Proof.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros. elim (gcd_lincomb a b 1).
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro alpha. intros. elim H2. intro beta. intros.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H0. intro y. intros.
(* Goal: ZDivides a c *)
(* Goal: not (@eq Z a Z0) *)
(* Goal: gcd a b (S O) *)
   split with (c * alpha + y * beta)%Z. rewrite Zmult_plus_distr_r.
(* Goal: @eq Z c (Z.add (Z.mul (Z.mul a c) alpha) (Z.mul a (Z.mul y beta))) *)
(* Goal: not (@eq Z a Z0) *)
(* Goal: gcd a b (S O) *)
   rewrite Zmult_assoc. rewrite Zmult_assoc.
(* Goal: @eq Z c (Z.add (Z.mul (Z.mul a c) alpha) (Z.mul (Z.mul a y) beta)) *)
(* Goal: not (@eq Z a Z0) *)
(* Goal: gcd a b (S O) *)
   rewrite <- H4. rewrite (Zmult_comm a c). rewrite (Zmult_comm b c).
(* Goal: Mod (Z.mul (Z.mul b c) rc) b p *)
(* Goal: Prime p *)
(* Goal: not (Mod c Z0 p) *)
   rewrite Zmult_assoc_reverse. rewrite Zmult_assoc_reverse.
(* Goal: @eq Z (Z.mul a beta) (Z.add (Z.mul a beta) (Z.add (Z.mul (Z.of_nat p) alpha) (Z.mul (Z.of_nat p) (Z.opp alpha)))) *)
(* Goal: not (@eq Z (Z.of_nat p) Z0) *)
(* Goal: gcd (Z.of_nat p) a (S O) *)
(* Goal: Prime p *)
   rewrite <- Zmult_plus_distr_r. transitivity (c * 1)%Z.
(* Goal: @eq Z (Z.mul b (Zpos xH)) b *)
(* Goal: Prime p *)
(* Goal: not (Mod c Z0 p) *)
   rewrite Zmult_comm. rewrite Zmult_1_l. reflexivity.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   apply (f_equal (A:=Z)). assumption. assumption. assumption.
Qed.

Lemma primedivmult :
 forall p n m : nat,
 Prime p -> Divides p (n * m) -> Divides p n \/ Divides p m.
Proof.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros. elim (prime_div_or_gcd1 p (Z_of_nat n)).
(* Goal: or (@eq nat qi qi) (exlist nat (fun b : nat => @eq nat qi b) restqs) *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   left. rewrite <- (abs_inj p). rewrite <- (abs_inj n).
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   apply zdivdiv. assumption.
(* Goal: or (@eq nat qj qi) (exlist nat (fun b : nat => @eq nat qj b) restqs) *)
(* Goal: Divides a (multDrop qj (Cons nat qi restqs)) *)
(* Goal: lt O y *)
(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   right. rewrite <- (abs_inj p). rewrite <- (abs_inj m).
(* Goal: Divides (Z.abs_nat (Z.of_nat p)) (Z.abs_nat (Z.of_nat m)) *)
(* Goal: Prime p *)
   apply zdivdiv. apply divmultgcd with (Z_of_nat n).
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H. intros. apply Zgt_neq.
(* Goal: Z.gt (Z.of_nat p) Z0 *)
(* Goal: gcd (Z.of_nat p) a (S O) *)
(* Goal: Prime p *)
   change (Z_of_nat p > Z_of_nat 0)%Z in |- *. apply Znat.inj_gt.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   apply gt_trans with 1. assumption. unfold gt in |- *. unfold lt in |- *. apply le_n.
(* Goal: ZDivides (Z.of_nat p) (Z.of_nat (Init.Nat.mul n m)) *)
(* Goal: gcd (Z.of_nat p) (Z.of_nat n) (S O) *)
(* Goal: Prime p *)
   rewrite <- Znat.inj_mult. apply divzdiv. rewrite abs_inj. rewrite abs_inj.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption. assumption. assumption.
Qed.

Lemma mod_mult_inv_r :
 forall (a : Z) (p : nat),
 Prime p -> ~ Mod a 0 p -> exists ra : Z, Mod (a * ra) 1 p.
Proof.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros. elim (prime_div_or_gcd1 p a).

   (* case p divides a *)
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro. elim H0. elim H1. intros. split with x. simpl in |- *. assumption.

   (* case gcd(p,a)=1 *)
(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro. elim (gcd_lincomb (Z_of_nat p) a 1).
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro alpha. intros. elim H2. intro beta. intros.
(* Goal: @ex Z (fun ra : Z => Mod (Z.mul a ra) (Zpos xH) p) *)
(* Goal: not (@eq Z (Z.of_nat p) Z0) *)
(* Goal: gcd (Z.of_nat p) a (S O) *)
(* Goal: Prime p *)
   unfold Mod in |- *. split with beta. split with (- alpha)%Z.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   simpl in H3. rewrite H3.
(* Goal: @eq Z (Z.mul a beta) (Z.add (Z.add (Z.mul (Z.of_nat p) alpha) (Z.mul a beta)) (Z.mul (Z.of_nat p) (Z.opp alpha))) *)
(* Goal: not (@eq Z (Z.of_nat p) Z0) *)
(* Goal: gcd (Z.of_nat p) a (S O) *)
(* Goal: Prime p *)
   rewrite (Zplus_comm (Z_of_nat p * alpha)). rewrite Zplus_assoc_reverse.
(* Goal: @eq Z (Z.mul a beta) (Z.add (Z.mul a beta) (Z.add (Z.mul (Z.of_nat p) alpha) (Z.mul (Z.of_nat p) (Z.opp alpha)))) *)
(* Goal: not (@eq Z (Z.of_nat p) Z0) *)
(* Goal: gcd (Z.of_nat p) a (S O) *)
(* Goal: Prime p *)
   rewrite <- Zmult_plus_distr_r. rewrite Zplus_opp_r.
(* Goal: @eq nat qi qi *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   rewrite <- Zmult_0_r_reverse. rewrite <- Zplus_0_r_reverse. reflexivity.
(* Goal: not (@eq Z (Z.of_nat p) Z0) *)
(* Goal: gcd (Z.of_nat p) a (S O) *)
(* Goal: Prime p *)
   apply Zgt_neq. change (Z_of_nat p > Z_of_nat 0)%Z in |- *.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   apply Znat.inj_gt. apply gt_trans with 1. elim H. intros. assumption.
(* Goal: le (S O) (S O) *)
(* Goal: gcd (Z.of_nat p) a (S O) *)
(* Goal: Prime p *)
   unfold gt in |- *. unfold lt in |- *. apply le_n.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption. assumption.
Qed.

Lemma mod_mult_cancel_r :
 forall (a b c : Z) (p : nat),
 Prime p -> ~ Mod c 0 p -> Mod (a * c) (b * c) p -> Mod a b p.
Proof.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros. elim (mod_mult_inv_r c p). intro rc. intros.
(* Goal: Mod (Z.mul (Z.mul b c) rc) b p *)
(* Goal: Prime p *)
(* Goal: not (Mod c Z0 p) *)
   apply mod_trans with (a * c * rc)%Z. rewrite Zmult_assoc_reverse.
(* Goal: Mod a (Z.mul a (Z.mul c rc)) p *)
(* Goal: Mod (Z.mul (Z.mul a c) rc) b p *)
(* Goal: Prime p *)
(* Goal: not (Mod c Z0 p) *)
   pattern a at 1 in |- *. replace a with (a * 1)%Z. apply mod_mult_compat. apply mod_refl.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   apply mod_sym. assumption.
(* Goal: @eq Z (Z.mul b (Zpos xH)) b *)
(* Goal: Prime p *)
(* Goal: not (Mod c Z0 p) *)
   rewrite Zmult_comm. apply Zmult_1_l.
(* Goal: Mod (Z.mul (Z.mul a c) rc) b p *)
(* Goal: Prime p *)
(* Goal: not (Mod c Z0 p) *)
   apply mod_trans with (b * c * rc)%Z.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   apply mod_mult_compat. assumption. apply mod_refl. rewrite Zmult_assoc_reverse.
(* Goal: Mod (Z.mul b (Z.mul c rc)) (Z.mul b (Zpos xH)) p *)
(* Goal: @eq Z (Z.mul b (Zpos xH)) b *)
(* Goal: Prime p *)
(* Goal: not (Mod c Z0 p) *)
   pattern b at 2 in |- *. replace b with (b * 1)%Z. apply mod_mult_compat. apply mod_refl.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
(* Goal: @eq Z (Z.mul b (Zpos xH)) b *)
(* Goal: Prime p *)
(* Goal: not (Mod c Z0 p) *)
   rewrite Zmult_comm. apply Zmult_1_l.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption. assumption.
Qed.

Lemma mod_mult_0 :
 forall (p : nat) (a b : Z),
 Prime p -> Mod (a * b) 0 p -> Mod a 0 p \/ Mod b 0 p.
Proof.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: or (Mod a Z0 p) (Mod b Z0 p) *)
   elim (moddivmin (a * b) 0 p).
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: or (Mod a Z0 p) (Mod b Z0 p) *)
   rewrite <- Zminus_0_l_reverse in H1.
(* Goal: or (Mod a Z0 p) (Mod b Z0 p) *)
   rewrite abs_mult in H1.
(* Goal: or (Mod a Z0 p) (Mod b Z0 p) *)
   elim (primedivmult p (Zabs_nat a) (Zabs_nat b)).
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   left. elim (moddivmin a 0 p). intros.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   apply H5. rewrite <- Zminus_0_l_reverse. assumption.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   right. elim (moddivmin b 0 p). intros.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   apply H5. rewrite <- Zminus_0_l_reverse. assumption.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
(* Goal: Divides p (Init.Nat.mul (Z.abs_nat a) (Z.abs_nat b)) *)
   apply H1.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
Qed.

Lemma mod_not_exp_0 :
 forall p : nat,
 Prime p -> forall a : Z, ~ Mod a 0 p -> forall m : nat, ~ Mod (Exp a m) 0 p.
Proof.
(* Goal: forall (p : nat) (_ : Prime p) (a : Z) (_ : not (Mod a Z0 p)) (m : nat), not (Mod (Exp a m) Z0 p) *)
   intros p Hp a Ha. simple induction m.
(* Goal: exlist nat (fun b : nat => @eq nat qi b) (Cons nat qi restqs) *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   simpl in |- *. intro. elim (mod_0not1 p).
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim Hp. intros. assumption.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   apply mod_sym. assumption.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   simpl in |- *. intros. intro.
(* Goal: False *)
   elim (mod_mult_0 p a (Exp a n) Hp).
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption. assumption. assumption.
Qed.

(**
  This lemma simply states that: if a divides b where 0<a<b,
  then there is a prime factor qi of b such that a divides (b/qi).
  I.e. If you divide by a non-trivial divisor, then the other
  divisor contains a prime factor.
*)

Lemma techlemma3 :
 forall (qlist : natlist) (a b : nat),
 0 < a ->
 a < b ->
 Divides a b ->
 b = product qlist ->
 allPrime qlist ->
 exists qi : nat, inlist nat qi qlist /\ Divides a (multDrop qi qlist).
Proof.
(* Goal: forall (qlist : natlist) (a b : nat) (_ : lt O a) (_ : lt a b) (_ : Divides a b) (_ : @eq nat b (product qlist)) (_ : allPrime qlist), @ex nat (fun qi : nat => and (inlist nat qi qlist) (Divides a (multDrop qi qlist))) *)
   simple induction qlist.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   simpl in |- *. intros. rewrite H2 in H0.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   elim (lt_not_le a 1). assumption. unfold lt in H. assumption.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros qi restqs IH. intros.
(* Goal: @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   elim (divdec a qi).

   (* case (Divides qi a) *)

(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H1. intro x. intros.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H4. intro y. intros.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim (IH y (product restqs)). intro qj. intros.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H7. intros.
(* Goal: @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
(* Goal: lt O y *)
(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   split with qj.
(* Goal: and (inlist nat qi (Cons nat qi restqs)) (Divides a (multDrop qi (Cons nat qi restqs))) *)
   split.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   unfold inlist in |- *. simpl in |- *. right. assumption.
(* Goal: Divides a (multDrop qj (Cons nat qi restqs)) *)
(* Goal: lt O y *)
(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite H6.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H9. intro z. intros.
(* Goal: Divides (Init.Nat.mul qi y) (multDrop qj (Cons nat qi restqs)) *)
(* Goal: lt O y *)
(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   elim (eqdec qi qj).
(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro. rewrite H11. rewrite multdrop_cons_eq.
(* Goal: Divides (Init.Nat.mul qj y) (product restqs) *)
(* Goal: forall _ : not (@eq nat qi qj), Divides (Init.Nat.mul qi y) (multDrop qj (Cons nat qi restqs)) *)
(* Goal: lt O y *)
(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite <- (multdrop_mult restqs qj). split with z.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   rewrite mult_assoc_reverse. rewrite H10. reflexivity. assumption.

(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro. rewrite multdrop_cons_neq.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   split with z.
(* Goal: @eq nat (Init.Nat.mul qi (multDrop qj restqs)) (Init.Nat.mul (Init.Nat.mul qi y) z) *)
(* Goal: not (@eq nat qj qi) *)
(* Goal: lt O y *)
(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite mult_assoc_reverse.
(* Goal: @eq nat (Init.Nat.mul qi (multDrop qj restqs)) (Init.Nat.mul qi (Init.Nat.mul y z)) *)
(* Goal: not (@eq nat qj qi) *)
(* Goal: lt O y *)
(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite H10.
(* Goal: @eq nat qi qi *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   reflexivity.
(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro. elim H11. rewrite H12. reflexivity.

(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim (le_or_lt y 0). intro.
(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim (le_lt_or_eq y 0). intro.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   elim (lt_n_O y). assumption.
(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro. rewrite H8 in H6. rewrite <- mult_n_O in H6. rewrite H6 in H.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   elim (lt_n_O 0). assumption.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   intro. assumption.

(* Goal: lt y (product restqs) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   apply simpl_lt_mult_l with qi.
(* Goal: lt (Init.Nat.mul qi y) (Init.Nat.mul qi (product restqs)) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite <- H6.
(* Goal: Divides a (product restqs) *)
   simpl in H2.
(* Goal: lt a (Init.Nat.mul qi (product restqs)) *)
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite <- H2.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.

(* Goal: Divides a (product restqs) *)
   simpl in H2.
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite H5 in H2.
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite H6 in H2.
(* Goal: Divides y (product restqs) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   split with x.
(* Goal: @eq nat (product restqs) (Init.Nat.mul y x) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   rewrite mult_assoc_reverse in H2.
(* Goal: @eq nat (product restqs) (Init.Nat.mul a z) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   apply simpl_eq_mult_l with qi.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   unfold allPrime in H3.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   simpl in H3.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   elim H3.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul y x)) *)
(* Goal: @eq nat (product restqs) (product restqs) *)
(* Goal: allPrime restqs *)
(* Goal: forall _ : not (Divides qi a), @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   elim H7.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   apply lt_trans with 1.
(* Goal: lt O (S O) *)
(* Goal: lt (S O) qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   apply lt_O_Sn.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
   symmetry  in |- *.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
(* Goal: @eq nat qi qi *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   reflexivity.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   unfold allPrime in H3.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   simpl in H3.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   elim H3.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.

   (* case ~(Divides qi a) *)

(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: @ex nat (fun qi0 : nat => and (inlist nat qi0 (Cons nat qi restqs)) (Divides a (multDrop qi0 (Cons nat qi restqs)))) *)
   split with qi.
(* Goal: and (inlist nat qi (Cons nat qi restqs)) (Divides a (multDrop qi (Cons nat qi restqs))) *)
   split.
(* Goal: inlist nat qi (Cons nat qi restqs) *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   unfold inlist in |- *.
(* Goal: exlist nat (fun b : nat => @eq nat qi b) (Cons nat qi restqs) *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   simpl in |- *.
(* Goal: or (@eq nat qi qi) (exlist nat (fun b : nat => @eq nat qi b) restqs) *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   left.
(* Goal: @eq nat qi qi *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   elim (beq_nat_ok qi qi).
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: @eq nat qi qi *)
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   reflexivity.
(* Goal: Divides a (multDrop qi (Cons nat qi restqs)) *)
   rewrite multdrop_cons_eq.
(* Goal: Divides a (product restqs) *)
   elim H1.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: Divides a (product restqs) *)
   simpl in H2.
(* Goal: Divides a (product restqs) *)
   unfold Divides in |- *.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   unfold allPrime in H3.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   simpl in H3.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   elim H3.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
   elim (primedivmult qi a x H6).
(* Goal: forall _ : Divides qi a, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intro.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: forall _ : Divides qi x, @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H4.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H8. intro z. intros.
(* Goal: @ex nat (fun q : nat => @eq nat (product restqs) (Init.Nat.mul a q)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   split with z.
(* Goal: @eq nat (product restqs) (Init.Nat.mul a z) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   rewrite H2 in H5.
(* Goal: @eq nat (product restqs) (Init.Nat.mul a z) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   rewrite H9 in H5.
(* Goal: @eq nat (product restqs) (Init.Nat.mul a z) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   rewrite (mult_assoc a qi) in H5.
(* Goal: @eq nat (product restqs) (Init.Nat.mul a z) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   rewrite (mult_comm a) in H5.
(* Goal: @eq nat (product restqs) (Init.Nat.mul a z) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   rewrite (mult_assoc_reverse qi a) in H5.
(* Goal: @eq nat (product restqs) (Init.Nat.mul a z) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   apply simpl_eq_mult_l with qi.
(* Goal: lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   elim H6.
(* Goal: forall (_ : gt qi (S O)) (_ : forall (q : nat) (_ : Divides q qi), or (@eq nat q (S O)) (@eq nat q qi)), lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   intros.
(* Goal: lt O qi *)
(* Goal: @eq nat (Init.Nat.mul qi (product restqs)) (Init.Nat.mul qi (Init.Nat.mul a z)) *)
(* Goal: Divides qi (Init.Nat.mul a x) *)
   apply lt_trans with 1. apply lt_O_Sn.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   assumption.
(* Goal: @eq nat b (Init.Nat.mul qi (product restqs)) *)
   split with (product restqs). rewrite <- H5. assumption.
Qed.
