Require Import ZArith.
Set Implicit Arguments.
Unset Strict Implicit.

Section list_in_Type.
Variable A : Type.
 
Inductive listT : Type :=
  | nilT : listT
  | consT : A -> listT -> listT.
 
Fixpoint lengthT (l : listT) : nat :=
  match l return nat with
  | consT _ m => S (lengthT m)
  | _ => 0
  end.


Lemma lgt_eq_0_nil:forall (l : listT),lengthT l=0->l=nilT.
induction l.
simpl;auto.
simpl;intros.
absurd  (S (lengthT l) = 0);auto with * . 
Qed.
 

Definition tailT (l:listT) : listT :=
  match l with
  | nilT => nilT
  | consT a  m => m
  end.

(* le 0 ds A *)
Variable a0:A.

Definition headT (l:listT) :A:=
  match l with
  | nilT => a0
  | consT x  _ =>  x
  end.

Fixpoint mk_list_n_fst_elt(n:nat)(l:listT){struct n}:listT:=
   match n with 
      O=>nilT
     |S m=>match l with 
                     nilT=>nilT
                  |consT x xs=>consT x (mk_list_n_fst_elt m xs) end
   end.

Fixpoint sum_mult_list(plusA mulA:A->A->A)(l g:listT){struct l }:A:=
match l,g with 
   nilT       ,               _             =>a0
 |(consT x xs)   ,    nilT          =>a0
 |(consT x xs)  ,(consT y ys)=>plusA (mulA x y) (sum_mult_list plusA mulA xs ys) end.

Fixpoint InT (a : A) (l : listT) {struct l} : Prop :=
  match l with
  | nilT => False
  | consT b m => b = a \/ InT a m
  end.


Fixpoint InTeq (eq : A -> A -> Prop) (a : A) (l : listT) {struct l} : Prop :=
  match l with
  | nilT => False
  | consT b m => eq b a \/ InTeq eq a m
  end.

Lemma inT_consT : forall (a b : A) (l : listT), InT b l -> InT b (consT a l).
simpl in |- *; auto.
Qed.

Definition inclT (l m : listT) := forall a : A, InT a l -> InT a m.

Fixpoint appT (l m : listT) {struct l} : listT :=
  match l return listT with
  | nilT => m
  | consT a l1 => consT a (appT l1 m)
  end.
 
Definition is_nil (l : listT) :=
  match l with
  | nilT => True
  | consT _ _ => False
  end.


Fixpoint incT (l g : listT) {struct l} : Prop :=
  match l with
  | nilT => True
  | consT a ls => InT a g /\ incT ls g
  end.

Fixpoint eq_elt_list (a : A) (l : listT) {struct l} : Prop :=
  match l with
  | nilT => False
  | consT b ls => a = b \/ eq_elt_list a ls
  end.

Fixpoint not_eq_elt_list (l : listT) : Prop :=
  match l with
  | nilT => True
  | consT a l => ~ eq_elt_list a l /\ not_eq_elt_list l
  end.

End list_in_Type.
 
Fixpoint ith_elt(A:Type)(l:listT A)(n:nat)(o:A){struct l}:A:=
match l with 
  |nilT=>o
  |consT x xs=>match n with
		 |0=>o
		 |S 0=>x
		 |S m=>ith_elt xs m o 
	           end
  end.




Section mapT.
Variable A : Type.
Variable B : Type.
Variable f : A -> B.
 
Fixpoint mapT (l : listT A) : listT B :=
  match l with
  | nilT => nilT B
  | consT a t => consT (f a) (mapT t)
  end.
 
Fixpoint flatT(l:listT (listT A)):listT A:=match l with
   |nilT=>(nilT A)
   |(consT a ls)=>(appT a (flatT ls))
   end.

Fixpoint flat_mapT (A B : Type) (f : A -> listT B) 
 (l : listT A) {struct l} : listT B :=
  match l with
  | nilT => nilT B
  | consT x t => appT (f x) (flat_mapT f t)
  end.
 
End mapT.


Fixpoint ProdT_n(n:nat)(D:Type){struct n}:Type:=
  match n with 
    |0=>D
    |(S 0)=>D
    |(S m)=>prodT D (ProdT_n m D)
      end.



Inductive PdT(A:Type)(B:Type)(C:Type):Type:=
tripleT:A->B->C->PdT A B C .

Section pdT_proj.

   Variables A B C: Type.

  Definition FtT (H:PdT A B C) := match H with
                                   |tripleT  x _ _ => x
                                   end.
  Definition SdT (H:PdT A B C ) := match H with
                                   |tripleT _ y _ => y
                                   end.

 Definition TdT (H:PdT A B C ) := match H with
                                   |tripleT   _ _ x => x
                                   end.
 
Definition list_td_PdT(l:listT (PdT A B C)):listT C:=mapT TdT l.
End pdT_proj.


Inductive ProdT(A:Type)(B:Type)(C:Type)(D:Type):Type:=
quadT:A->B->C->D->ProdT A B C D.

Section prodT_proj.

   Variables A B C D: Type.

  Definition FstT (H:ProdT A B C D) := match H with
                                   | quadT x _ _ _=> x
                                   end.
  Definition SndT (H:ProdT A B C D) := match H with
                                   | quadT _ y _ _=> y
                                   end.

 Definition TrdT (H:ProdT A B C D) := match H with
                                   | quadT  _ _ x _=> x
                                   end.
  Definition FthT (H:ProdT A B C D) := match H with
                                   | quadT _ _ _ y => y
                                   end.

Definition list_fth_Prod(l:listT (ProdT A B C D)):listT D:=mapT FthT l.
End prodT_proj.


Fixpoint Prod_PS (A:Type)(A0:A)(n : nat) (listA : listT A) {struct n} : listT (listT A) :=
 match n with
   O => consT (consT A0 (nilT _)) (nilT _)
  | S m =>
      flatT
       (mapT
         (fun (x : A) => mapT (fun (y : listT A) => consT x y) (Prod_PS A0 m listA))
         listA)
 end.

							   

Section listprod.

Variables V W X: Type.
Variable l1 : listT V.
Fixpoint listTprod (l2 : listT W) : listT (prodT V W) :=
  match l2 with
  | nilT => nilT (prodT V W)
  | consT y ys => appT (mapT (fun z => pairT z y) l1) (listTprod ys)
  end.

Fixpoint listPd_fst_fix(a:V)(g:listT W)(h:listT X){struct h}:listT (PdT V W X):=
  match h with 
    |nilT=>nilT (PdT V W X)
    |consT y ys=>appT (mapT (fun z => tripleT a z y) g) (listPd_fst_fix a g ys)
end.


Fixpoint listPd (l:listT V)(g:listT W)(h:listT X){struct l}:listT (PdT V W X):=
  match l with 
    |nilT=>nilT (PdT V W X)
    |consT y ys=>appT (listPd_fst_fix y g h) (listPd ys g h) 
    end.


Lemma lgt_listp_not_eq:forall (E : listT V)(F: listT W)(G : listT X),
       lengthT E <> 0 -> lengthT F <> 0 -> lengthT G <> 0 -> lengthT (listPd E F G) <> 0.
induction E;induction F;induction G.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros.
auto with *.
Qed.

End listprod. 


Definition pred_cons (V : Type) (l : listT V) : Prop :=
  match l with
  | nilT => False
  | consT _ _ => True
  end.

Lemma not_cons_nil :
 forall (V : Type) (l : listT V) (n : V), consT n l <> nilT _.
red in |- *; intros.
assert (pred_cons (consT n l)).
simpl in |- *.
auto.
rewrite H in H0.
simpl in H0; intuition.
Qed.


Lemma not_app_cons_nil :
 forall (V : Type) (l : listT V) (n : V), appT l (consT n (nilT _)) <> nilT _.
simple induction l.
simpl in |- *.
intros.
apply not_cons_nil.
simpl in |- *; intros.
apply not_cons_nil.
Qed.


Lemma not_nil_cons :
 forall (V : Type) (l : listT V),
 l <> nilT _ -> exists g : listT V, (exists a : V, l = consT a g).
intros V l.
case l.
simpl in |- *; intros; intuition.
simpl in |- *; intros.
exists l0.
exists v.
auto.
Qed.







Lemma list_nil :
 forall (V W : Type) (l : listT V), listTprod (nilT W) l = nilT _.
simple induction l.
simpl in |- *.
auto with *.
simpl in |- *; intros.
auto.
Qed.

Lemma app_nil : forall (V : Type) (l : listT V), appT l (nilT _) = l.
simple induction l.
simpl in |- *.
auto with *.
simpl in |- *; intros.
rewrite H; auto with *.
Qed.

Lemma inT_ :
 forall (V : Type) (h g : listT V) (a : V),
 InT a (appT h g) -> InT a h \/ InT a g.
simple induction h.
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
elim H0.
intro; intuition.
intro.
generalize (H g a0 H1).
intro; intuition.
Qed.

Lemma inT_impl :
 forall (V : Type) (h : listT V) (a : V),
 InT a h -> forall g : listT V, InT a (appT h g).
simple induction h.
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
intuition.
Qed.

Lemma inT_impl2 :
 forall (V : Type) (h : listT V) (a : V),
 InT a h -> forall g : listT V, InT a (appT g h).
intros.
induction  g as [| a0 g Hrecg].
simpl in |- *; intros.
auto.
simpl in |- *.
auto.
Qed.



Lemma inT_app_impl_ :
 forall (V : Type) (l g h : listT V) (a b : V),
 InT a (appT l g) -> InT a (appT l (consT b (appT h g))).
simple induction l.
simpl in |- *; intros.
right.
apply inT_impl2.
auto.
simpl in |- *; intros.
intuition.
Qed.

Lemma inT_app_impl :
 forall (V : Type) (l g h j : listT V) (a b : V),
 InT a (appT l g) -> InT a (appT l (consT b (appT h (appT j g)))).
simple induction l.
simpl in |- *; intros.
right.
apply inT_impl2.
apply inT_impl2.
auto.
simpl in |- *; intros.
intuition.
Qed.


Lemma incT_cons :
 forall (W : Type) (g h : listT W) (a : W), incT g h -> incT g (consT a h).
simple induction g.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
split.
intuition.
apply H.
intuition.
Qed.

Lemma inc_app :
 forall (W : Type) (l g h : listT W) (a : W),
 incT g h -> incT (appT l g) (consT a (appT l h)).
simple induction l.
simpl in |- *; intros.
apply incT_cons.
auto.
simpl in |- *; intros.
split.
intuition.
generalize (H g h a H0).
intro.
apply incT_cons.
auto.
Qed.

Lemma inT_map :
 forall (V W : Type) (l : listT W) (a0 : V) (c : W),
 InT c l -> InT (pairT a0 c) (mapT (fun z : W => pairT a0 z) l).
simple induction l.
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
elim H0.
intro heq; rewrite heq; intuition.
intro; right; apply H; auto.
Qed.

Lemma in_list :
 forall (V W : Type) (g : listT W) (a : V) (c : W),
 InT c g -> InT (pairT a c) (listTprod (consT a (nilT _)) g).
simple induction g.
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
elim H0.
intro heq; rewrite heq; intuition.
intro.
right.
apply H.
auto.
Qed.

Lemma flat_map_nil:forall (A:Type)(l:listT A),(flatT (mapT (fun _:A=>(nilT (listT A))) l))=nilT _.
induction l;simpl;intros;auto.
Qed.


Lemma not_nil_inT :
 forall (V : Type) (a : V) (u : listT V), InT a u -> u <> nilT _.
simple induction u.
simpl in |- *; intros; intuition.
simpl in |- *; intros.
apply not_cons_nil.
Qed.

Axiom
  incT_impl :
    forall (V W : Type) (t l : listT (prodT V W)) (a : prodT V W),
    incT t (consT a l) ->
    InT a t /\ incT t l \/ InT a t /\ ~ incT t l \/ incT t l.




Lemma inT_app_ :
 forall (V W : Type) (x : listT V) (a : W) (l : listT W) (c : V),
 InT c x ->
 InT (pairT a c) (appT (mapT (fun z => pairT a z) x) (listTprod l x)).
simple induction x.
simpl in |- *; intros; intuition.
simpl in |- *; intros.
elim H0.
intro heq; rewrite heq; intuition.
intro.
case l0.
generalize (H a0 (nilT _) c H1).
simpl in |- *.
rewrite list_nil.
rewrite app_nil.
intro; intuition.
simpl in |- *; intros.
generalize (H a0 l1 c H1).
simpl in |- *; intros.
right.
apply inT_app_impl_.
auto.
Qed.


Lemma lgt_app :
 forall (W : Type) (l g : listT W),
 lengthT (appT l g) = lengthT l + lengthT g.
simple induction l.
simpl in |- *; intros; auto with *.
simpl in |- *; intros; auto with *.
Qed.


Lemma listp_nil :
 forall (V W : Type) (l : listT W), listTprod (nilT V) l = nilT (prodT V W).
simple induction l.
simpl in |- *; intros; auto with *.
simpl in |- *; intros; auto with *.
Qed.



Lemma lgt_listp_cons_eq :
 forall (V W : Type) (g : listT W) (l : listT V) (a : V),
 lengthT (listTprod (consT a l) g) =
 lengthT (appT (mapT (fun z : W => pairT a z) g) (listTprod l g)).
simple induction g.
simpl in |- *.
intros; case l; auto with *.
simpl in |- *; intros.
case l0.
simpl in |- *.
rewrite listp_nil.
auto.
simpl in |- *.
intros.
rewrite lgt_app.
rewrite H.
simpl in |- *.
rewrite listp_nil.
rewrite lgt_app.
simpl in |- *; auto.
intros.
rewrite lgt_app.
rewrite lgt_app.
rewrite lgt_app.
rewrite H.
rewrite lgt_app.
auto with *.
Qed.

Lemma lgt_map :
 forall (V W: Type) (l : listT V) (a : W),
 lengthT (mapT (fun z : V => pairT a z) l) = lengthT l.
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
auto with *.
Qed.



Lemma lgt_map_cons :
 forall (V : Type) (l g: listT V) ,
 lengthT (mapT (fun z : V => consT z g) l) = lengthT l.
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
auto with *.
Qed.

Lemma lgt_map_cons_:
 forall (V : Type) (l: listT (listT V))(z:V) ,
 lengthT (mapT (fun g : listT V => consT z g) l) = lengthT l.
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
auto with *.
Qed.


Lemma lgt_map_ :
 forall (V W: Type) (l : listT V) (a : W),
 lengthT (mapT (fun z : V => pairT z a) l) = lengthT l.
simple induction l.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
auto with *.
Qed.

Lemma lgt_listp:forall (V W : Type) (g : listT W) (l : listT V),
 lengthT (listTprod  l g) =
 (lengthT l) *(lengthT g).
induction g.
induction l.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_app.
simpl.
rewrite lgt_map_.
rewrite IHg.
rewrite plus_comm.
auto with * .
Qed.





Lemma mapT_app :
 forall (T V : Type) (l g : listT T) (f : T -> V),
 mapT f (appT l g) = appT (mapT f l) (mapT f g).
simple induction l.
simpl in |- *.
auto with *.
simpl in |- *; intros.
rewrite H; auto with *.
Qed.

(*returns True if P x for all x in l *) 
Fixpoint ListPred (A : Type) (P : A->Prop) (l : listT A) {struct l} : Prop :=
  match l with
  | nilT => True
  | consT x xs => P x /\ ListPred P xs
  end.

(*returns True if P x for at least an elt x in l *) 
Fixpoint ListPred_or (A : Type) (P : A->Prop) (l : listT A) {struct l} : Prop :=
  match l with
  | nilT => False
  | consT x xs => P x \/ListPred_or P xs
  end.

Fixpoint ListPred_Or (A B: Type) (P : A->B->Prop) (l : listT A)(g:listT B) {struct l} : Prop :=
  match l with
  | nilT => False
  | consT x xs => match g with 
		    | nilT => False
		    | consT y ys => (P x y) \/ListPred_Or P xs ys
		  end
  end.


Lemma lgt_flat_map:forall (T V : Type) (l  : listT T) (g  : listT V),
lengthT (flatT (mapT (fun z : T=>mapT (fun w : V=> pairT z w) g) l))=
(lengthT l) * (lengthT g).
induction l.
induction g.
simpl;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_app.
rewrite lgt_map.
rewrite IHl.
auto.
Qed.

Lemma lgt_flat_map_cons:forall ( V : Type) (l  : listT V)(g  :listT (listT V)),
lengthT (flatT (mapT (fun z : V=>mapT (fun w : listT V=> consT z w) g) l))=
(lengthT l) * (lengthT g).
induction l.
induction g.
simpl;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_app.
rewrite lgt_map_cons_.
rewrite IHl.
auto.
Qed.



Lemma lgt_app_map_eq:forall (V W:Type)(a:V)(l:listT V)(g:listT W),(lengthT
         (appT
            (mapT (fun y : W => pairT a y) g)
            (flatT
               (mapT
                  (fun x : V =>
                   mapT (fun y : W => pairT x y)
                     g) l))))=(lengthT g)+(lengthT g)*(lengthT l).
intros.
rewrite lgt_app.
rewrite lgt_map.
rewrite lgt_flat_map.
auto with * . 
Qed.

Section ListPred.
Variable A : Type.
Variable P : A ->  Prop.
Variable l : listT A.
Hypothesis H : forall (a : A), InT a l ->  P a.
 
Lemma listPred_impl: ListPred P l.
induction l.
simpl; auto.
simpl; intros.
split.
apply H.
simpl.
left; auto.
apply IHl0.
intros.
apply H.
simpl.
auto.
Qed.
 
End ListPred.


Section listprod_.

Variable V : Type.
Lemma listTprod_lengthT :
 forall l1 l2 : listT V, lengthT l1 * lengthT l2 = lengthT (listTprod l1 l2).
simple induction l1.
simple induction l2.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
rewrite lgt_listp_cons_eq.
rewrite lgt_app.
rewrite H.
rewrite lgt_map.
auto.
Qed.


End listprod_.


Section list_min.
Variable T : Type.
Variable min_T : T -> T ->  T.
 
Definition list_min (a : T) (l : listT T) : listT T := mapT (min_T a) l.
(* returns the listT of all fi-fj  1<=i<j<=lengthT l*)
 
Fixpoint gen_coll_test (l : listT T) : listT T :=
 match l with
   nilT => nilT _
  | consT x xs => appT (list_min x xs) (gen_coll_test xs)
 end.
 

Lemma lgt_list_min: forall (a :T) (l : listT T),lengthT (list_min a l)=lengthT l.
induction l.
simpl;intros;auto.
simpl;intros.
auto with *.
Qed.

End list_min.


Section listTprod.

Variable V W X: Type.


Lemma lgt_listPd_fix_nil:forall (a:V)(l0:listT W), lengthT (listPd_fst_fix a (nilT V) l0)=0.
induction l0.
simpl;intros;auto.
simpl;intros;auto.
Qed.

Lemma lgt_map_tr_eq:forall (a:V)(a1:W)(l0:listT V),(lengthT (mapT (fun z : V => tripleT a z a1) l0))=(lengthT l0).
induction l0.
simpl;intros;auto.
simpl;intros;auto.
Qed.

Lemma mult_S:forall a b c :nat,a*b*(S c)=a*b*c+a*b.
intros.
auto with * . 
Qed.

Lemma eq_mult_S:forall a c  :nat,a*(S c)=a*c+a.
intros.
auto with * . 
Qed.

Lemma mult_S_eq:forall a b c :nat,a+(b+c*S b)*S a=b+(a+(b+c*S b)*a)+c*S b.
intros.
rewrite Mult.mult_plus_distr_r.
rewrite Mult.mult_plus_distr_r.
rewrite Plus.plus_assoc.
rewrite Plus.plus_assoc.
rewrite Plus.plus_assoc.
rewrite mult_S.
rewrite Plus.plus_assoc.
rewrite eq_mult_S.
rewrite Plus.plus_assoc.
auto with * .
Qed.

Lemma listTprod_lengthT_ :
 forall (l1 l2 : listT V)(l3:listT W), lengthT l1 * lengthT l2*lengthT l3 = lengthT (listPd l1 l2 l3).
simple induction l1.
simple induction l2.
simple induction l3.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
auto.
simpl in |- *; intros.
auto.
simple induction l2.
simple induction l3.
simpl in |- *; intros.
rewrite <-H.
simpl.
auto.
simpl in |- *; intros.
rewrite lgt_app.
rewrite lgt_listPd_fix_nil.
rewrite <-H.
simpl.
auto.
simple induction l3.
simpl in |- *; intros.
rewrite <-H.
simpl.
auto with * .
simpl in |- *; intros.
rewrite lgt_app.
rewrite lgt_app.
simpl.
rewrite <-H.
simpl.
rewrite lgt_app in H1.
rewrite <-H in H1.
simpl in H1.
rewrite lgt_map_tr_eq.
rewrite mult_S.
replace 
     (lengthT l0 + lengthT (listPd_fst_fix a (consT a0 l0) l4) +
      (lengthT l * S (lengthT l0) * lengthT l4 + lengthT l * S (lengthT l0))) with
     (lengthT l0 + (lengthT (listPd_fst_fix a (consT a0 l0) l4) +
      (lengthT l * S (lengthT l0) * lengthT l4)) + lengthT l * S (lengthT l0)).
rewrite <-H1.
rewrite mult_S_eq.
auto with * .
auto with * .
Qed.

Lemma mult_eq_0_:forall a b:nat,a=0\/b=0->a*b=0.
intros.
elim H.
intro h;rewrite h;simpl;auto with * . 
intro h;rewrite h;simpl;auto with * . 
Qed.


Lemma mult_eq_0:forall a b:nat,a*b=0->a=0\/b=0.
intros a b.
case a.
simpl;intros;auto.
case b.
simpl;intros;auto.
simpl;intros.
absurd (S (n + n0 * S n) = 0);auto with * .
Qed.

Lemma lgt_listPS:forall (V W:Type)(l:listT V)(g:listT W),
lengthT l<>0->lengthT g<>0->
lengthT (listTprod l g)<>0.
intros.
rewrite lgt_listp.
assert (~((lengthT l)=0\/(lengthT g)=0)).
intuition.
generalize (mult_eq_0 (a:=lengthT l)(b:=lengthT g)).
intro.
intuition.
Qed.


End listTprod.


Lemma listPd_nil:forall (U V W:Type)(l:listT U)(g:listT V),(listPd l g (nilT W))=nilT _.
induction l.
induction g.
simpl;auto.
simpl;auto.
induction g.
simpl;auto.
simpl;auto.
Qed.


Lemma listPd_nil1:forall (U V W:Type)(l:listT W)(g:listT V),(listPd (nilT U) l g )=nilT _.
induction l.
simpl;auto.
induction g.
simpl;auto.
simpl.
auto.
Qed.

Lemma lgt_0_eq_nil:forall (U:Type)(l:listT U),lengthT l=0->l=nilT U.
induction l;simpl;auto.
intro.
absurd (S (lengthT l) = 0);auto with * . 
Qed.

Lemma list_fix_nil:forall (U V W:Type)(a:U)(l:listT W),(listPd_fst_fix a (nilT V) l)=nilT _.
induction l;simpl;auto.
Qed.

(* return the nb of times of P is true in l *)
Fixpoint nb_P_true(T:Type)(l:listT T)(P:T->Prop)(dec_P:forall x:T,{P x}+{~P x}){struct l}:nat:=
match l with 
          nilT => 0
       |consT x xs=>match (dec_P x) with 
                                      left _=>S (nb_P_true xs dec_P)
                                   |right _=>(nb_P_true  xs dec_P) end
  end.


Lemma ListPred_appT_l:
 forall (A : Type) (a b : listT A) (P : A ->  Prop),
 ListPred P a /\ ListPred P b ->  ListPred P (appT a b).
simple induction a.
simpl; intros; intuition.
simpl; intros.
intuition.
Qed.
 
Lemma ListPred_appT_r:
 forall (A : Type) (a b : listT A) (P : A ->  Prop),
 ListPred P (appT a b) ->  ListPred P a /\ ListPred P b.
simple induction a.
simpl; intros; intuition.
simpl; intros.
assert (ListPred P l /\ ListPred P b).
apply H.
intuition.
intuition.
Qed.

(*return all the list at m elt from l *)
Fixpoint ss_liste(A:Type)(l:listT A)(m:nat){struct l}:listT (listT A):=
  match l with
   |nilT => match m with
               |O => consT (nilT _) (nilT _)
               |S m' =>(nilT _) end
   |consT hd tl => match m with
               |O => consT (nilT _) (nilT _)
               |S m' =>appT (mapT (fun u => consT hd  u) (ss_liste tl m')) (ss_liste tl m)
               end
   end .


Require Import Binomials.

Lemma lgt_ss_liste:forall (A:Type)(list:listT A)(l:nat),
lengthT (ss_liste list l)=binomial (lengthT list) l.
induction list.
simpl;intro l;case l;intuition.
simpl;intro.
case l.
simpl;intros;intuition.
simpl;intro.
rewrite lgt_app.
rewrite lgt_map_cons_.
intros.
rewrite IHlist.
rewrite IHlist.
auto with * .
Qed.