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


(**
   list.
   Polymorphic lists with some operations.
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import Arith.
Require Import ZArith.
Require Import EqNat.

Require Import dec.
Require Import natZ.

(** * Polymorphic lists *)

Inductive list (A : Set) : Set :=
  | Nil : list A
  | Cons : A -> list A -> list A.

(** Length of a list *)

Fixpoint length (A : Set) (l : list A) {struct l} : nat :=
  match l with
  | Nil => 0
  | Cons a r => S (length A r)
  end.

Lemma length_0 : forall (A : Set) (l : list A), length A l = 0 -> l = Nil A.
Proof.
(* Goal: forall (A : Set) (l : list A) (n : nat) (_ : @eq nat (length A l) (S n)), @ex A (fun h : A => @ex (list A) (fun t : list A => and (@eq (list A) l (Cons A h t)) (@eq nat (length A t) n))) *)
   intros A l. case l.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   reflexivity.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros. discriminate H.
Qed.

Lemma length_S :
 forall (A : Set) (l : list A) (n : nat),
 length A l = S n ->
 exists h : A, (exists t : list A, l = Cons A h t /\ length A t = n).
Proof.
(* Goal: forall (A : Set) (l : list A) (n : nat) (_ : @eq nat (length A l) (S n)), @ex A (fun h : A => @ex (list A) (fun t : list A => and (@eq (list A) l (Cons A h t)) (@eq nat (length A t) n))) *)
   intros A l. case l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros. discriminate H.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros h0 t0 n H. injection H. intro. 
(* Goal: @ex A (fun h : A => @ex (list A) (fun t : list A => and (@eq (list A) (Cons A h0 t0) (Cons A h t)) (@eq nat (length A t) n))) *)
   split with h0. split with t0. split.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   reflexivity. assumption.
Qed.

(** Map a function over a list *)

Fixpoint map (A B : Set) (f : A -> B) (l : list A) {struct l} : 
 list B :=
  match l with
  | Nil => Nil B
  | Cons a r => Cons B (f a) (map A B f r)
  end.

Notation Map := (map _ _) (only parsing).

Lemma map_length :
 forall (A B : Set) (f : A -> B) (l : list A),
 length A l = length B (map A B f l).
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   simpl in |- *. reflexivity.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   simpl in |- *. intros. rewrite H. reflexivity.
Qed.

(** Checks that all members of a list are P *)

Fixpoint alllist (A : Set) (P : A -> Prop) (qlist : list A) {struct qlist} :
 Prop :=
  match qlist with
  | Nil => True
  | Cons m l => P m /\ alllist A P l
  end.

Lemma alllist_dec :
 forall (A : Set) (P : A -> Prop) (l : list A),
 (forall x : A, P x \/ ~ P x) -> alllist A P l \/ ~ alllist A P l.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. left. trivial.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intros h t IH H. simpl in |- *.
(* Goal: @ex A (fun q0 : A => and (or (@eq A q0 q) (exlist A (fun b : A => @eq A q0 b) l)) (P q0)) *)
(* Goal: forall _ : @ex A (fun q : A => and (inlist A q qlist) (P q)), exlist A P qlist *)
   elim IH. elim (H h).
(* Goal: and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x)) *)
(* Goal: exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t) *)
   left. split. assumption. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   right. intro. apply H0. elim H2. intros. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   right. intro. apply H0. elim H1. intros. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption.
Qed.

(** Checks that some member of a list is P *)

Fixpoint exlist (A : Set) (P : A -> Prop) (qlist : list A) {struct qlist} :
 Prop :=
  match qlist with
  | Nil => False
  | Cons m l => P m \/ exlist A P l
  end.

Lemma exlist_dec :
 forall (A : Set) (P : A -> Prop) (l : list A),
 (forall x : A, P x \/ ~ P x) -> exlist A P l \/ ~ exlist A P l.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. right. intro. assumption.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intros h t IH H. simpl in |- *.
(* Goal: or (or (P h) (exlist A P t)) (not (or (P h) (exlist A P t))) *)
   elim (H h).
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   left. left. assumption.
(* Goal: @ex A (fun q0 : A => and (or (@eq A q0 q) (exlist A (fun b : A => @eq A q0 b) l)) (P q0)) *)
(* Goal: forall _ : @ex A (fun q : A => and (inlist A q qlist) (P q)), exlist A P qlist *)
   elim IH.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   left. right. assumption.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   right. intro. elim H2.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption.
Qed.

(** Membership *)

Definition inlist (A : Set) (a : A) := exlist A (fun b : A => a = b).

Lemma inlist_head_eq :
 forall (A : Set) (x y : A) (l : list A), x = y -> inlist A x (Cons A y l).
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intros. unfold inlist in |- *. simpl in |- *.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   left. assumption.
Qed.

Lemma inlist_head_neq :
 forall (A : Set) (x y : A) (l : list A),
 x <> y -> (inlist A x (Cons A y l) <-> inlist A x l).
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intros. unfold inlist in |- *. simpl in |- *.
(* Goal: and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x)) *)
(* Goal: exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t) *)
   split.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. elim H0. intro. elim H. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. right. assumption.
Qed.

Lemma inlist_tail :
 forall (A : Set) (x y : A) (l : list A),
 inlist A x l -> inlist A x (Cons A y l).
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intros. unfold inlist in |- *. simpl in |- *. right. assumption.
Qed.

Lemma inlist_dec :
 forall (A : Set) (x : A) (l : list A),
 (forall a b : A, a = b \/ a <> b) -> inlist A x l \/ ~ inlist A x l.
Proof.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. unfold inlist in |- *.
(* Goal: or (exlist A (fun b : A => @eq A x b) l) (not (exlist A (fun b : A => @eq A x b) l)) *)
   apply exlist_dec. exact (H x).
Qed.

(** alllist and exlist behave nicely *)

Theorem alllist_ok :
 forall (A : Set) (P : A -> Prop) (qlist : list A),
 alllist A P qlist <-> (forall q : A, inlist A q qlist -> P q).
Proof.
(* Goal: and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x)) *)
(* Goal: exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t) *)
   split.

   (* -> *)
(* Goal: forall _ : @ex A (fun q : A => and (inlist A q qlist) (P q)), exlist A P qlist *)
   elim qlist.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros. elim H0.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros q l IH H. elim H. intros. elim H2.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. rewrite H3. assumption.  
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. apply IH. assumption. assumption.

   (* <- *)
(* Goal: forall _ : @ex A (fun q : A => and (inlist A q qlist) (P q)), exlist A P qlist *)
   elim qlist.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros. trivial.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros q l IH H. split.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   apply H. left. reflexivity.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   apply IH. intros. apply H. right. assumption.
Qed.

Theorem exlist_ok :
 forall (A : Set) (P : A -> Prop) (qlist : list A),
 exlist A P qlist <-> (exists q : A, inlist A q qlist /\ P q).
Proof.
(* Goal: and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x)) *)
(* Goal: exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t) *)
   split.

   (* -> *)
(* Goal: forall _ : @ex A (fun q : A => and (inlist A q qlist) (P q)), exlist A P qlist *)
   elim qlist.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros. elim H.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros q l IH H. elim H.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intro. split with q. split. left. reflexivity. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intro. elim IH. intros q1 Hq1. elim Hq1. intros. split with q1.
(* Goal: and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x)) *)
(* Goal: exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t) *)
   split. right. assumption. assumption. assumption.

   (* <- *)
(* Goal: forall _ : @ex A (fun q : A => and (inlist A q qlist) (P q)), exlist A P qlist *)
   elim qlist.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros. elim H. intros. elim H0. intros. elim H1.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros q l IH H. elim H.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros q1 Hq1. elim Hq1. intros. elim H0.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. left. rewrite <- H2. assumption.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. right. apply IH. split with q1. split. assumption. assumption.
Qed.

(** * Lists of natural numbers. *)

Definition natlist := list nat.

(** Multiply all elements of a natlist *)

Fixpoint product (qlist : natlist) : nat :=
  match qlist with
  | Nil => 1
  | Cons m l => m * product l
  end.

(** Drop the first occurance of q from qlist *)

Fixpoint drop (q : nat) (qlist : natlist) {struct qlist} : natlist :=
  match qlist with
  | Nil => Nil nat
  | Cons q' l => if beq_nat q q' then l else Cons nat q' (drop q l)
  end.

(** Multiply all elements of qlist, except for (first occurance of) q *)

Definition multDrop (q : nat) (l : natlist) := product (drop q l).

Lemma multdrop_cons_eq :
 forall (q : nat) (l : natlist), multDrop q (Cons nat q l) = product l.
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold multDrop in |- *. simpl in |- *. intros. elim (beq_nat_eq q q). intros.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite H. reflexivity. reflexivity.
Qed.

Lemma multdrop_cons_neq :
 forall (p q : nat) (l : natlist),
 p <> q -> multDrop p (Cons nat q l) = q * multDrop p l.
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold multDrop in |- *. simpl in |- *. intros. elim (beq_nat_neq p q). intros.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite H0. simpl in |- *. reflexivity. assumption.
Qed.

Lemma multdrop_mult :
 forall (qlist : natlist) (q : nat),
 inlist nat q qlist -> q * multDrop q qlist = product qlist.
Proof.
(* Goal: forall (q : nat) (qlist : natlist), @eq Z (Z.of_nat (multDrop q qlist)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat qlist)) *)
   simple induction qlist.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros. elim H.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros q1 l IH. intros. elim (eqdec q q1).

   (* case q=q1 *)
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intro. rewrite H0. rewrite multdrop_cons_eq. reflexivity.

   (* case ~q=q1 *)
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. rewrite multdrop_cons_neq.
(* Goal: @eq Z (Z.mul q (Z.mul q1 (zmultDrop q l))) (Z.mul q1 (zproduct l)) *)
(* Goal: not (@eq Z q q1) *)
   rewrite <- (IH q). rewrite mult_assoc.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite (mult_comm q q1). rewrite mult_assoc. reflexivity.
(* Goal: forall (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   unfold inlist in H. simpl in H. elim H.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. elim H0. assumption.  
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption.
Qed.

(** * Lists of integers. *)

Definition Zlist := list Z.

(** allPos checks whether all members of a Zlist are non-negative. *)

Definition allPos : Zlist -> Prop := alllist Z (fun x : Z => (x >= 0)%Z).

(** Multiply all elements of a Zlist *)

Fixpoint zproduct (l : Zlist) : Z :=
  match l with
  | Nil => 1%Z
  | Cons x t => (x * zproduct t)%Z
  end.

Lemma productzproduct :
 forall l : natlist, Z_of_nat (product l) = zproduct (map nat Z Z_of_nat l).
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   simpl in |- *. reflexivity.
(* Goal: forall (a : nat) (l : list nat) (_ : @eq (list nat) (map Z nat Z.abs_nat (map nat Z Z.of_nat l)) l), @eq (list nat) (Cons nat (Z.abs_nat (Z.of_nat a)) (map Z nat Z.abs_nat (map nat Z Z.of_nat l))) (Cons nat a l) *)
   intros h t IH.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. rewrite <- IH.
(* Goal: @eq Z (Z.of_nat (Init.Nat.mul h (multDrop q t))) (Z.mul (Z.of_nat h) (Z.of_nat (multDrop q t))) *)
(* Goal: not (@eq Z (Z.of_nat q) (Z.of_nat h)) *)
(* Goal: not (@eq nat q h) *)
   rewrite Znat.inj_mult.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   reflexivity.
Qed.

Lemma zproductproduct :
 forall l : Zlist, Zabs_nat (zproduct l) = product (map Z nat Zabs_nat l).
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   simpl in |- *. reflexivity.
(* Goal: forall (a : nat) (l : list nat) (_ : @eq (list nat) (map Z nat Z.abs_nat (map nat Z Z.of_nat l)) l), @eq (list nat) (Cons nat (Z.abs_nat (Z.of_nat a)) (map Z nat Z.abs_nat (map nat Z Z.of_nat l))) (Cons nat a l) *)
   intros h t IH.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. rewrite abs_mult.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite IH. reflexivity.
Qed.

(** Drop an element from a Zlist *)

Fixpoint zdrop (x : Z) (l : Zlist) {struct l} : Zlist :=
  match l with
  | Nil => Nil Z
  | Cons h t => if Zeq_bool x h then t else Cons Z h (zdrop x t)
  end.

Lemma zdrop_head_eq :
 forall (x y : Z) (l : Zlist), x = y -> zdrop x (Cons Z y l) = l.
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros. elim (zeq_bool_eq x y). intros.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite H0. reflexivity. assumption.
Qed.

Lemma zdrop_head_neq :
 forall (x y : Z) (l : Zlist),
 x <> y -> zdrop x (Cons Z y l) = Cons Z y (zdrop x l).
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros. elim (zeq_bool_neq x y). intros.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite H0. reflexivity. assumption.
Qed.

Lemma zdrop_length :
 forall (x : Z) (l : Zlist),
 inlist Z x l -> S (length Z (zdrop x l)) = length Z l.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros. elim H.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros h t IH. intros. elim (zeqdec x h).

   (* case x=h *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intro. simpl in |- *. elim (zeq_bool_eq x h).
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. rewrite H1. reflexivity. assumption.

   (* case x<>h *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intro. simpl in |- *. elim (zeq_bool_neq x h).
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. rewrite H1. simpl in |- *. rewrite IH. reflexivity.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   elim H. intros. elim H0. assumption. intros. assumption. assumption.
Qed.

Lemma zdrop_neq_inlist :
 forall (x y : Z) (l : Zlist),
 x <> y -> inlist Z x l -> inlist Z x (zdrop y l).
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. elim H0.
(* Goal: forall (a : nat) (l : list nat) (_ : @eq (list nat) (map Z nat Z.abs_nat (map nat Z Z.of_nat l)) l), @eq (list nat) (Cons nat (Z.abs_nat (Z.of_nat a)) (map Z nat Z.abs_nat (map nat Z Z.of_nat l))) (Cons nat a l) *)
   intros h t IH.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. elim (zeqdec x h).
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. rewrite zdrop_head_neq.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   apply inlist_head_eq. assumption.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   rewrite <- H1. intro. apply H. symmetry  in |- *. assumption.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. elim (zeqdec y h).
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. rewrite zdrop_head_eq.
(* Goal: inlist Z x t *)
(* Goal: not (@eq Z x h) *)
(* Goal: not (@eq Z y h) *)
   elim (inlist_head_neq Z x h t).
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. apply H3. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. rewrite zdrop_head_neq.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   elim (inlist_head_neq Z x h (zdrop y t)). intros.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   apply H4. apply IH. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   elim (inlist_head_neq Z x h t). intros.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   apply H5. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption. assumption.
Qed.

Lemma zdrop_inlist_weak :
 forall (x y : Z) (l : Zlist), inlist Z x (zdrop y l) -> inlist Z x l.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intro. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros h t IH. intros.
(* Goal: forall _ : inlist Z x (Cons Z h t), @eq Z (Z.mul x (zproduct (zdrop x (Cons Z h t)))) (zproduct (Cons Z h t)) *)
   elim (zeqdec x h).
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intro. rewrite H0. unfold inlist in |- *. simpl in |- *. left. reflexivity.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. elim (zeqdec y h).
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. rewrite H1 in H. rewrite zdrop_head_eq in H.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   apply inlist_tail. assumption. reflexivity.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. rewrite zdrop_head_neq in H.
(* Goal: forall (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   unfold inlist in H. simpl in H. elim H.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. elim H0. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. apply inlist_tail. apply IH. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption.
Qed.

Lemma zdrop_swap :
 forall (x y : Z) (l : Zlist), zdrop x (zdrop y l) = zdrop y (zdrop x l).
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   simpl in |- *. reflexivity.
(* Goal: forall (a : nat) (l : list nat) (_ : @eq (list nat) (map Z nat Z.abs_nat (map nat Z Z.of_nat l)) l), @eq (list nat) (Cons nat (Z.abs_nat (Z.of_nat a)) (map Z nat Z.abs_nat (map nat Z Z.of_nat l))) (Cons nat a l) *)
   intros h t IH.
(* Goal: forall _ : inlist Z x (Cons Z h t), @eq Z (Z.mul x (zproduct (zdrop x (Cons Z h t)))) (zproduct (Cons Z h t)) *)
   elim (zeqdec x h). elim (zeqdec y h).

   (* y=h, x=h *)
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. rewrite H. rewrite H0. reflexivity.

   (* y<>h, x=h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros.
(* Goal: @eq Zlist (zdrop x (zdrop y (Cons Z h t))) (zdrop y (zdrop x (Cons Z h t))) *)
(* Goal: forall _ : not (@eq Z x h), @eq Zlist (zdrop x (zdrop y (Cons Z h t))) (zdrop y (zdrop x (Cons Z h t))) *)
   rewrite (zdrop_head_eq x h t).
(* Goal: @eq Zlist (zdrop x (zdrop y (Cons Z h t))) (zdrop y t) *)
(* Goal: @eq Z x h *)
(* Goal: forall _ : not (@eq Z x h), @eq Zlist (zdrop x (zdrop y (Cons Z h t))) (zdrop y (zdrop x (Cons Z h t))) *)
   rewrite (zdrop_head_neq y h t).
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite zdrop_head_eq. reflexivity.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption. assumption.

(* Goal: forall (_ : not (@eq Z x h)) (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   elim (zeqdec y h).

   (* y=h, x<>h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros.
(* Goal: @eq Zlist (zdrop x (zdrop y (Cons Z h t))) (zdrop y (zdrop x (Cons Z h t))) *)
(* Goal: forall (_ : not (@eq Z y h)) (_ : not (@eq Z x h)), @eq Zlist (zdrop x (zdrop y (Cons Z h t))) (zdrop y (zdrop x (Cons Z h t))) *)
   rewrite (zdrop_head_eq y h).
(* Goal: @eq Zlist (Cons Z h (zdrop x (zdrop y t))) (zdrop y (zdrop x (Cons Z h t))) *)
(* Goal: not (@eq Z x h) *)
(* Goal: not (@eq Z y h) *)
   rewrite (zdrop_head_neq x h).
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite zdrop_head_eq. reflexivity.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption. assumption.

   (* y<>h, x<>h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros.
(* Goal: @eq Zlist (Cons Z h (zdrop x (zdrop y t))) (zdrop y (Cons Z h (zdrop x t))) *)
(* Goal: not (@eq Z x h) *)
(* Goal: not (@eq Z x h) *)
(* Goal: not (@eq Z y h) *)
   rewrite (zdrop_head_neq y h).
(* Goal: @eq Zlist (Cons Z h (zdrop x (zdrop y t))) (zdrop y (zdrop x (Cons Z h t))) *)
(* Goal: not (@eq Z x h) *)
(* Goal: not (@eq Z y h) *)
   rewrite (zdrop_head_neq x h).
(* Goal: @eq Zlist (Cons Z h (zdrop x (zdrop y t))) (zdrop y (zdrop x (Cons Z h t))) *)
(* Goal: not (@eq Z x h) *)
(* Goal: not (@eq Z y h) *)
   rewrite (zdrop_head_neq x h).
(* Goal: @eq Zlist (Cons Z h (zdrop x (zdrop y t))) (zdrop y (Cons Z h (zdrop x t))) *)
(* Goal: not (@eq Z x h) *)
(* Goal: not (@eq Z x h) *)
(* Goal: not (@eq Z y h) *)
   rewrite (zdrop_head_neq y h).
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite IH. reflexivity.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption.
Qed.

Lemma zdrop_inlist_swap :
 forall (x y : Z) (l : Zlist),
 inlist Z y l -> inlist Z x (zdrop y l) -> inlist Z y (zdrop x l).
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intro H. elim H.
(* Goal: forall (a : nat) (l : list nat) (_ : @eq (list nat) (map Z nat Z.abs_nat (map nat Z Z.of_nat l)) l), @eq (list nat) (Cons nat (Z.abs_nat (Z.of_nat a)) (map Z nat Z.abs_nat (map nat Z Z.of_nat l))) (Cons nat a l) *)
   intros h t IH.
(* Goal: forall _ : inlist Z x (Cons Z h t), @eq Z (Z.mul x (zproduct (zdrop x (Cons Z h t)))) (zproduct (Cons Z h t)) *)
   elim (zeqdec x h). elim (zeqdec y h).

   (* y=h,x=h *)
(* Goal: forall (_ : not (@eq Z y h)) (_ : not (@eq Z x h)) (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   intros Hyh Hxh. rewrite Hyh. rewrite Hxh.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. assumption.

   (* y<>h,x=h *)
(* Goal: forall (_ : not (@eq Z y h)) (_ : not (@eq Z x h)) (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   intros Hyh Hxh.
(* Goal: forall (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   rewrite (zdrop_head_neq y).
(* Goal: forall (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (Cons Z h (zdrop y t))), inlist Z y (zdrop x (Cons Z h t)) *)
(* Goal: not (@eq Z y h) *)
(* Goal: forall (_ : not (@eq Z x h)) (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   rewrite (zdrop_head_eq x).
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. elim (inlist_head_neq Z y h t).
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. apply H1. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption. assumption.

(* Goal: forall (_ : not (@eq Z x h)) (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   elim (zeqdec y h).

   (* y=h,x<>h *)
(* Goal: forall (_ : not (@eq Z y h)) (_ : not (@eq Z x h)) (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   intros Hyh Hxh.
(* Goal: forall (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
(* Goal: forall (_ : not (@eq Z y h)) (_ : not (@eq Z x h)) (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   rewrite (zdrop_head_eq y).
(* Goal: forall (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (Cons Z h (zdrop y t))), inlist Z y (zdrop x (Cons Z h t)) *)
(* Goal: not (@eq Z y h) *)
   rewrite (zdrop_head_neq x).
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. apply inlist_head_eq. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption.

   (* y<>h, x<>h *)
(* Goal: forall (_ : not (@eq Z y h)) (_ : not (@eq Z x h)) (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   intros Hyh Hxh.
(* Goal: forall (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (zdrop y (Cons Z h t))), inlist Z y (zdrop x (Cons Z h t)) *)
   rewrite (zdrop_head_neq y).
(* Goal: forall (_ : inlist Z y (Cons Z h t)) (_ : inlist Z x (Cons Z h (zdrop y t))), inlist Z y (zdrop x (Cons Z h t)) *)
(* Goal: not (@eq Z y h) *)
   rewrite (zdrop_head_neq x).
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. elim (inlist_head_neq Z y h (zdrop x t)).
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. apply H2. apply IH.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   elim (inlist_head_neq Z y h t). intros.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   apply H3. assumption. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   elim (inlist_head_neq Z x h (zdrop y t)). intros.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   apply H3. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption. assumption. assumption.
Qed.

Lemma zdrop_product :
 forall (x : Z) (l : Zlist),
 inlist Z x l -> (x * zproduct (zdrop x l))%Z = zproduct l.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intro. elim H.
(* Goal: forall (a : nat) (l : list nat) (_ : @eq (list nat) (map Z nat Z.abs_nat (map nat Z Z.of_nat l)) l), @eq (list nat) (Cons nat (Z.abs_nat (Z.of_nat a)) (map Z nat Z.abs_nat (map nat Z Z.of_nat l))) (Cons nat a l) *)
   intros h t IH. elim (zeqdec x h).
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. rewrite zdrop_head_eq.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite H. reflexivity. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. rewrite zdrop_head_neq.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. rewrite Zmult_assoc.
(* Goal: @eq Z (Z.mul (Z.mul x h) (zproduct (zdrop x t))) (Z.mul h (zproduct t)) *)
(* Goal: not (@eq Z x h) *)
   rewrite Zmult_comm with x h.
(* Goal: @eq Z (Z.mul (Z.mul h x) (zproduct (zdrop x t))) (Z.mul h (zproduct t)) *)
(* Goal: not (@eq Z x h) *)
   rewrite Zmult_assoc_reverse.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite IH. reflexivity.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   elim inlist_head_neq with Z x h t. intros.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   apply H1. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption.
Qed.

(** Multiply all elements except first occurance of x *)

Definition zmultDrop (x : Z) (l : Zlist) := zproduct (zdrop x l).

Lemma zmultdrop_cons_eq :
 forall (q : Z) (l : Zlist), zmultDrop q (Cons Z q l) = zproduct l.
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold zmultDrop in |- *. simpl in |- *. intros. elim (zeq_bool_eq q q). intros.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite H. reflexivity. reflexivity.
Qed.

Lemma zmultdrop_cons_neq :
 forall (p q : Z) (l : Zlist),
 p <> q -> zmultDrop p (Cons Z q l) = (q * zmultDrop p l)%Z.
Proof.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold zmultDrop in |- *. simpl in |- *. intros. elim (zeq_bool_neq p q). intros.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite H0. simpl in |- *. reflexivity. assumption.
Qed.

Lemma zmultdrop_mult :
 forall (qlist : Zlist) (q : Z),
 inlist Z q qlist -> (q * zmultDrop q qlist)%Z = zproduct qlist.
Proof.
(* Goal: forall (q : nat) (qlist : natlist), @eq Z (Z.of_nat (multDrop q qlist)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat qlist)) *)
   simple induction qlist.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros. elim H.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros q1 l IH. intros. elim (zeqdec q q1).

   (* case q=q1 *)
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intro. rewrite H0. rewrite zmultdrop_cons_eq. reflexivity.

   (* case ~q=q1 *)
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. rewrite zmultdrop_cons_neq.
(* Goal: @eq Z (Z.mul q (Z.mul q1 (zmultDrop q l))) (Z.mul q1 (zproduct l)) *)
(* Goal: not (@eq Z q q1) *)
   rewrite <- (IH q). rewrite Zmult_assoc.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite (Zmult_comm q q1). rewrite Zmult_assoc. reflexivity.
(* Goal: forall (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   unfold inlist in H. simpl in H. elim H.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. elim H0. assumption.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption.
Qed.

Lemma multdropzmultdrop :
 forall (q : nat) (qlist : natlist),
 Z_of_nat (multDrop q qlist) =
 zmultDrop (Z_of_nat q) (map nat Z Z_of_nat qlist).
Proof.
(* Goal: forall (q : nat) (qlist : natlist), @eq Z (Z.of_nat (multDrop q qlist)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat qlist)) *)
   simple induction qlist.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   simpl in |- *. reflexivity. 
(* Goal: forall (a : nat) (l : list nat) (_ : @eq Z (Z.of_nat (multDrop q l)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat l))), @eq Z (Z.of_nat (multDrop q (Cons nat a l))) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat (Cons nat a l))) *)
   intros h t.
(* Goal: forall _ : @eq Z (Z.of_nat (multDrop q t)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat t)), @eq Z (Z.of_nat (multDrop q (Cons nat h t))) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat (Cons nat h t))) *)
   elim (eqdec q h).

   (* q=h *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intro H. rewrite H. simpl in |- *.
(* Goal: forall _ : @eq Z (Z.of_nat (multDrop h t)) (zmultDrop (Z.of_nat h) (map nat Z Z.of_nat t)), @eq Z (Z.of_nat (multDrop h (Cons nat h t))) (zmultDrop (Z.of_nat h) (Cons Z (Z.of_nat h) (map nat Z Z.of_nat t))) *)
(* Goal: forall (_ : not (@eq nat q h)) (_ : @eq Z (Z.of_nat (multDrop q t)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat t))), @eq Z (Z.of_nat (multDrop q (Cons nat h t))) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat (Cons nat h t))) *)
   rewrite multdrop_cons_eq.
(* Goal: forall _ : @eq Z (Z.of_nat (multDrop h t)) (zmultDrop (Z.of_nat h) (map nat Z Z.of_nat t)), @eq Z (Z.of_nat (product t)) (zmultDrop (Z.of_nat h) (Cons Z (Z.of_nat h) (map nat Z Z.of_nat t))) *)
(* Goal: forall (_ : not (@eq nat q h)) (_ : @eq Z (Z.of_nat (multDrop q t)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat t))), @eq Z (Z.of_nat (multDrop q (Cons nat h t))) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat (Cons nat h t))) *)
   rewrite zmultdrop_cons_eq.
(* Goal: forall _ : @eq Z (Z.of_nat (multDrop h t)) (zmultDrop (Z.of_nat h) (map nat Z Z.of_nat t)), @eq Z (Z.of_nat (product t)) (zproduct (map nat Z Z.of_nat t)) *)
(* Goal: forall (_ : not (@eq nat q h)) (_ : @eq Z (Z.of_nat (multDrop q t)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat t))), @eq Z (Z.of_nat (multDrop q (Cons nat h t))) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat (Cons nat h t))) *)
   rewrite productzproduct.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intro IH. reflexivity.

   (* ~q=h *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   intro H. simpl in |- *.
(* Goal: forall _ : @eq Z (Z.of_nat (multDrop q t)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat t)), @eq Z (Z.of_nat (multDrop q (Cons nat h t))) (zmultDrop (Z.of_nat q) (Cons Z (Z.of_nat h) (map nat Z Z.of_nat t))) *)
   rewrite multdrop_cons_neq.
(* Goal: forall _ : @eq Z (Z.of_nat (multDrop q t)) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat t)), @eq Z (Z.of_nat (Init.Nat.mul h (multDrop q t))) (zmultDrop (Z.of_nat q) (Cons Z (Z.of_nat h) (map nat Z Z.of_nat t))) *)
(* Goal: not (@eq nat q h) *)
   rewrite zmultdrop_cons_neq.
(* Goal: @eq Z (Z.of_nat (Init.Nat.mul h (multDrop q t))) (Z.mul (Z.of_nat h) (zmultDrop (Z.of_nat q) (map nat Z Z.of_nat t))) *)
(* Goal: not (@eq Z (Z.of_nat q) (Z.of_nat h)) *)
(* Goal: not (@eq nat q h) *)
   intro IH. rewrite <- IH.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite Znat.inj_mult. reflexivity.
(* Goal: forall _ : exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t), @ex Z (fun x : Z => and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x))) *)
   intro. apply H.
(* Goal: @eq nat q h *)
(* Goal: not (@eq nat q h) *)
   rewrite <- (abs_inj q). rewrite <- (abs_inj h).
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite H0. reflexivity.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption.
Qed.

(** Multiply all elements in list with a *)

Definition mapmult (a : Z) (l : Zlist) := map Z Z (fun x : Z => (a * x)%Z) l.

Lemma mapmult_image :
 forall (a : Z) (l : Zlist) (x : Z),
 inlist Z x l -> inlist Z (a * x)%Z (mapmult a l).
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   unfold mapmult in |- *. unfold inlist in |- *. simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros. assumption.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros h t IH. intros. elim H.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   left. rewrite H0. reflexivity.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   right. apply IH. assumption.
Qed.

Lemma mapmult_orig :
 forall (a : Z) (l : Zlist) (y : Z),
 inlist Z y (mapmult a l) -> exists x : Z, inlist Z x l /\ y = (a * x)%Z.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   unfold mapmult in |- *. unfold inlist in |- *. simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros. elim H.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros h t IH. intros.
(* Goal: forall (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   elim H.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intro. split with h. split. left. reflexivity. assumption.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intro. elim (IH y). intros. elim H1. intros.
(* Goal: and (or (@eq Z x h) (exlist Z (fun b : Z => @eq Z x b) t)) (@eq Z y (Z.mul a x)) *)
(* Goal: exlist Z (fun b : Z => @eq Z y b) (map Z Z (fun x : Z => Z.mul a x) t) *)
   split with x. split. right.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption. assumption.
Qed.

(** Lift inject_nat and absolu to natlist and Zlist. *)

Lemma abs_inj_list :
 forall l : natlist, map _ _ Zabs_nat (map _ _ Z_of_nat l) = l.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   simpl in |- *. reflexivity.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros h t IH.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite abs_inj. rewrite IH. reflexivity.
Qed.

Lemma inj_abs_pos_list :
 forall l : Zlist, allPos l -> map _ _ Z_of_nat (map _ _ Zabs_nat l) = l.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   simpl in |- *. intros. reflexivity.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   simpl in |- *. intros h t IH H. elim H. intros.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   rewrite inj_abs_pos. rewrite IH. reflexivity.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   assumption. assumption.
Qed.

Lemma inlist_inj_abs_pos_list :
 forall (q : nat) (l : Zlist),
 allPos l -> inlist nat q (map Z nat Zabs_nat l) -> inlist Z (Z_of_nat q) l.
Proof.
(* Goal: forall (q : nat) (l : Zlist) (_ : allPos l) (_ : inlist nat q (map Z nat Z.abs_nat l)), inlist Z (Z.of_nat q) l *)
   simple induction l.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. simpl in |- *. intros. assumption.
(* Goal: forall (a : Z) (l : list Z) (_ : forall (_ : alllist Z (fun x : Z => Z.ge x Z0) l) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat l)), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) l) (_ : alllist Z (fun x : Z => Z.ge x Z0) (Cons Z a l)) (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat (Cons Z a l))), exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) (Cons Z a l) *)
   unfold inlist in |- *. unfold allPos in |- *. simpl in |- *.
(* Goal: forall (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros h t IH Hp H. elim Hp. elim H.
(* Goal: @eq Z h h *)
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   left. rewrite H0. rewrite inj_abs_pos. reflexivity.
(* Goal: Z.ge h Z0 *)
(* Goal: forall (_ : exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t)) (_ : Z.ge h Z0) (_ : alllist Z (fun x : Z => Z.ge x Z0) t), or (@eq Z (Z.of_nat q) h) (exlist Z (fun b : Z => @eq Z (Z.of_nat q) b) t) *)
   intros. assumption.
(* Goal: exlist nat (fun b : nat => @eq nat q b) (map Z nat Z.abs_nat t) *)
   right. apply IH. assumption. assumption.
Qed.
