Require Import prob.
Require Import Reals.
Require Import listT.
Require Import R_lemma.
Require Import SchwartzExt.
Require Import Schwartz_Pol2Expr.
Require Import POLY_ax. 


Set Implicit Arguments.
Unset Strict Implicit.

Section col.


Axiom dec_ex:forall (A:Set)(a:A),{exists t:A,a=t}+{~(exists t:A,a=t)}.


Lemma dec_InT:forall (T:Set)(l:listT T),{exists t:T,InT t l}+{~(exists t:T,InT t l)}.
induction l.
simpl.
right.
red;intro.
elim H.
intros;intuition.
simpl;intros.
elim IHl.
intro;left.
elim a0.
intros.
exists x.
intuition.
intro.
case (dec_ex a).
intro;left.
elim e;intros.
exists x.
intuition.
intro.
right.
red;intro.
elim H.
intros.
elim H0.
intro.
red in n.
apply n.
exists x.
auto.
intro.
red in b.
apply b.
exists x.
auto.
Qed.

Require Import Ring_cat.
Require Import Pol_is_ring.

Variable Zq_ring:RING.
Definition Zq:Type:=Zq Zq_ring.
Variable Expr:Set->Type.
Variable A:Set.
(*card A=n*)
Variable n:nat.

Variable Call:CALL Zq.
Variable transl:Expr A -> Poly n Call.
Variable Fins2list : (A ->  Zq) ->  listT Zq.

Hypotheses dec_Evalstozero:
 forall (e : Expr A) (x : A ->  Zq),
  ({ Evalstozero transl Fins2list x e }) + ({ ~ Evalstozero transl Fins2list x e }).


Lemma dec_Ev0:forall (f:A ->Zq)(e:Expr A),{Evalstozero transl Fins2list f e}+{~(Evalstozero transl Fins2list f e)}.
intros.
apply (dec_Evalstozero  e f).
Qed.

Lemma dec_Ev0_InT:forall (f:A ->Zq)(l:listT (Expr A)),{exists e:(Expr A),InT e l/\Evalstozero transl Fins2list  f e}+
{~(exists e:(Expr A),InT e l/\Evalstozero transl Fins2list f e)}.
induction l.
simpl.
right.
red;intro.
elim H.
intros;intuition.
simpl;intros.
case (dec_Ev0 f a).
left.
exists a.
intuition.
intros.
elim IHl.
intros.
left.
elim a0.
intros.
exists x.
intuition.
intros.
right.
intro.
apply b.
elim H.
intros.
destruct H0.
destruct H0.
subst a.
intuition.
exists x.
intuition.
Qed.

Variable Ef:listT (A->Zq).
Hypotheses length_Ef:lengthT Ef<>0.

(* Pr[(a=0\/Eq0 l0)/\~(Eq0 l0)]= Pr[a=0/\~(Eq0 l0)] *)
 Lemma inter_Eq0_Simpl:
 forall (a : Expr A) (l0 : listT (Expr A)),
  Proba
   (A ->  Zq) Ef
   (EventInter
     (A ->  Zq)
     (EventUnion
       (A ->  Zq) (Ev_Evalstozero dec_Evalstozero a)
       (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)))
     (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0))))
  =
  Proba
   (A ->  Zq) Ef
   (EventInter
     (A ->  Zq) (Ev_Evalstozero dec_Evalstozero a)
     (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)))).
intros.
unfold Proba.
elim Ef.
simpl; auto with *.
simpl; intros.
change
 (lengthT
  (if event_inter_aux (A -> Zq)
        (EventUnion (A -> Zq)
           (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
              (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
              dec_Evalstozero a)
           (EvUnList (A -> Zq)
              (mapT
                 (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                    (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                    dec_Evalstozero) l0)))
        (Eventdiff (A -> Zq)
           (EvUnList (A -> Zq)
              (mapT
                 (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                    (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                    dec_Evalstozero) l0))) a0
   then
    consT a0
      (filter (A -> Zq)
         (EventInter (A -> Zq)
            (EventUnion (A -> Zq)
               (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                  (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                  dec_Evalstozero a)
               (EvUnList (A -> Zq)
                  (mapT
                     (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                        (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                        dec_Evalstozero) l0)))
            (Eventdiff (A -> Zq)
               (EvUnList (A -> Zq)
                  (mapT
                     (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                        (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                        dec_Evalstozero) l0)))) l)
   else
    filter (A -> Zq)
      (EventInter (A -> Zq)
         (EventUnion (A -> Zq)
            (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
               (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
               dec_Evalstozero a)
            (EvUnList (A -> Zq)
               (mapT
                  (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                     (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                     dec_Evalstozero) l0)))
         (Eventdiff (A -> Zq)
            (EvUnList (A -> Zq)
               (mapT
                  (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                     (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                     dec_Evalstozero) l0)))) l) =
lengthT
  (if event_inter_aux (A -> Zq)
        (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call) (Expr:=Expr)
           (transl:=transl) (Fins2list:=Fins2list) dec_Evalstozero a)
        (Eventdiff (A -> Zq)
           (EvUnList (A -> Zq)
              (mapT
                 (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                    (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                    dec_Evalstozero) l0))) a0
   then
    consT a0
      (filter (A -> Zq)
         (EventInter (A -> Zq)
            (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
               (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
               dec_Evalstozero a)
            (Eventdiff (A -> Zq)
               (EvUnList (A -> Zq)
                  (mapT
                     (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                        (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                        dec_Evalstozero) l0)))) l)
   else
    filter (A -> Zq)
      (EventInter (A -> Zq)
         (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call) (Expr:=Expr)
            (transl:=transl) (Fins2list:=Fins2list) dec_Evalstozero a)
         (Eventdiff (A -> Zq)
            (EvUnList (A -> Zq)
               (mapT
                  (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                     (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                     dec_Evalstozero) l0)))) l)).
case
 (event_inter_aux (A -> Zq)
        (EventUnion (A -> Zq)
           (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
              (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
              dec_Evalstozero a)
           (EvUnList (A -> Zq)
              (mapT
                 (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                    (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                    dec_Evalstozero) l0)))
        (Eventdiff (A -> Zq)
           (EvUnList (A -> Zq)
              (mapT
                 (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                    (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                    dec_Evalstozero) l0))) a0).
case
 (event_inter_aux (A -> Zq)
        (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call) (Expr:=Expr)
           (transl:=transl) (Fins2list:=Fins2list) dec_Evalstozero a)
        (Eventdiff (A -> Zq)
           (EvUnList (A -> Zq)
              (mapT
                 (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                    (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                    dec_Evalstozero) l0))) a0).
simpl; intros.
auto with *.
simpl; intros.
intuition.
case
 (event_inter_aux (A -> Zq)
        (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call) (Expr:=Expr)
           (transl:=transl) (Fins2list:=Fins2list) dec_Evalstozero a)
        (Eventdiff (A -> Zq)
           (EvUnList (A -> Zq)
              (mapT
                 (Ev_Evalstozero (n:=n) (Zq_ring:=Zq_ring) (Call:=Call)
                    (Expr:=Expr) (transl:=transl) (Fins2list:=Fins2list)
                    dec_Evalstozero) l0))) a0).
simpl; intros.
intuition.
simpl; intros.
auto with *.
Qed.

(* a=0/\~(Union x in l0 x=0) <-> a=0/\ (Inter x in l0 ~(x=0)) 
  i.e   A/\(~\/Bi)<->A/\(/\~Bi)  *)
 Lemma inter_Eq0_simpl:
 forall (a : Expr A) (l0 : listT (Expr A)) (x : A ->  Zq),
  (EventInter
    (A ->  Zq) (Ev_Evalstozero dec_Evalstozero a)
    (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0))) x
   <->
   EventInter
    (A ->  Zq) (Ev_Evalstozero dec_Evalstozero a)
    (EvIntList (A ->  Zq) (EvDiffList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)))
    x).
simple induction l0.
simpl; intros.
intuition.
simpl; intros.
unfold iff.
split.
intros.
split.
intuition.
split.
intuition.
unfold iff in H |-.
elim (H x).
intros.
intuition.
intros.
unfold iff in H |-.
elim (H x).
intros.
intuition.
Qed.

(* ~\/Ai<->/\~Ai *)
 Lemma diff_Eq0_simpl:
 forall (l0 : listT (Expr A)) (x : A ->  Zq),
  (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)) x <->
   EvIntList (A ->  Zq) (EvDiffList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)) x).
simple induction l0.
simpl; intros.
intuition.
simpl; intros.
unfold iff.
split.
intros.
split.
intuition.
unfold iff in H |-.
elim (H x).
intros.
intuition.
intros.
unfold iff in H |-.
elim (H x).
intros.
intuition.
Qed.
 

(* the event exists p in l s.t p=0 *)
 Definition Eq0 (l : listT (Expr A)) :=
   EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l).

Lemma proba_cond_PrcondList:
 forall (a : Expr A) (l0 : listT (Expr A)),
  prob_cond (A ->  Zq) Ef (Eq0 (consT a l0)) (Eventdiff (A ->  Zq) (Eq0 l0))
  = PrCondList (A ->  Zq) Ef (Ev_Evalstozero dec_Evalstozero a) (mapT (Ev_Evalstozero dec_Evalstozero) l0).
intros.
unfold Eq0.
simpl.
unfold PrCondList.
assert
 (prob_cond
   (A ->  Zq) Ef
   (EventUnion
     (A ->  Zq) (Ev_Evalstozero dec_Evalstozero a)
     (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)))
   (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0))) =
  prob_cond
   (A ->  Zq) Ef (Ev_Evalstozero dec_Evalstozero a)
   (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)))).
unfold prob_cond.
unfold prob.
rewrite inter_Eq0_Simpl.
auto with *.
change
 (prob_cond
   (A ->  Zq) Ef
   (EventUnion
     (A ->  Zq) (Ev_Evalstozero dec_Evalstozero a)
     (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)))
   (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0))) =
  prob_cond
   (A ->  Zq) Ef (Ev_Evalstozero dec_Evalstozero a)
   (EvIntList (A ->  Zq) (EvDiffList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)))).
rewrite H.
unfold prob_cond.
assert
 (prob
   (A ->  Zq) Ef
   (EventInter
     (A ->  Zq) (Ev_Evalstozero dec_Evalstozero a)
     (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0))))
  =
  prob
   (A ->  Zq) Ef
   (EventInter
     (A ->  Zq) (Ev_Evalstozero dec_Evalstozero a)
     (EvIntList (A ->  Zq) (EvDiffList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0))))).
apply prob_equiv.
apply length_Ef.
apply inter_Eq0_simpl.
rewrite H0.
assert
 (prob
   (A ->  Zq) Ef
   (Eventdiff (A ->  Zq) (EvUnList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0))) =
  prob
   (A ->  Zq) Ef
   (EvIntList (A ->  Zq) (EvDiffList (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l0)))).
apply prob_equiv.
apply length_Ef.
apply diff_Eq0_simpl.
rewrite H1.
auto with *.
Qed.

(* Pr[(Eq0 (a::l))/\~(Eq0 l)]<=Pr(a=0 | (Eq0 l)) *)
 Lemma prob_list:
 forall (a : Expr A) (l0 : listT (Expr A)),
 prob (A ->  Zq) Ef (Eventdiff (A ->  Zq) (Eq0 l0)) <> 0%R ->
  (INR
    (Proba
      (A ->  Zq) Ef
      (EventInter
        (A ->  Zq) (Eq0 (consT a l0)) (Eventdiff (A ->  Zq) (Eq0 l0)))) *
   / INR (lengthT Ef) <=
   PrCondList (A ->  Zq) Ef (Ev_Evalstozero dec_Evalstozero a) (mapT (Ev_Evalstozero dec_Evalstozero) l0))%R.
intros.
rewrite <- proba_cond_PrcondList.
unfold prob_cond.
rewrite <- Rmult_1_r with ( r :=
                          (INR
                            (Proba
                              (A ->  Zq) Ef
                              (EventInter
                                (A ->  Zq) (Eq0 (consT a l0))
                                (Eventdiff (A ->  Zq) (Eq0 l0)))) *
                           / INR (lengthT Ef))%R ).
rewrite Rdiv_Rmult.
apply Rmult_le_compat.
generalize (prob_sup0 (A->Zq) Ef length_Ef).
intro.
unfold prob in H |-.
apply H0
     with
      ( a :=
      EventInter
       (A ->  Zq) (Eq0 (consT a l0)) (Eventdiff (A ->  Zq) (Eq0 l0)) ).
auto with *.
unfold prob.
auto with *.
apply Rinv_prob_sup1.
apply length_Ef.
auto with *.
Qed.



Definition deg_Expr:Expr A->nat:=degre_Expr transl.
Variable q:nat.
Hypotheses Q: (0 < INR q)%R.

(* schwartz 's lemma:
  for a polynomial p 
  Pr(p(x1,...,xn)=0)<=degre p / card X  where x1,..,xn belong to X and p is non identically null *)
Hypotheses schwartz_:
   forall (p:Poly n Call),
~(eq_pol p (pol_null n Call))->
               (prob _ Ef (Ev_eq_pol0 Fins2list  p)<=INR (degre  Zq Call n p)/INR q)%R. 


(* Pr(Eq0 l)<=#l*d/(q-(#l-1)*d) *)
Lemma prob_eq0:
 forall (l : listT (Expr A)) (d : nat),
 ListPred (Exprnon0 transl Fins2list) l ->
 ListPred
  (fun p => deg_Expr p <= d)  l->
 (INR (lengthT l * d) / INR q < 1)%R ->
  (prob (A ->  Zq) Ef (Eq0 l) <=
   (INR (lengthT l) * INR d) / (INR q - (INR (lengthT l) - 1) * INR d))%R.
simple induction l.
simpl.
intros.
rewrite Rmult_0_l.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
unfold Eq0; simpl.
unfold prob.
rewrite evt_nul.
intros.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
auto with *.
intros.
unfold prob.
rewrite Prob_distr with ( M := Eq0 l0 ).
rewrite Rdiv_Rmult.
rewrite plus_INR.
rewrite Rmult_comm.
rewrite Rmult_plus_distr_l.
rewrite Rmult_comm.
rewrite Rmult_comm with ( r1 := (/ INR (lengthT Ef))%R ).
apply Rle_trans
     with
      ( r2 :=
      (INR d / (INR q - INR (lengthT l0) * INR d) +
       (INR (lengthT l0) * INR d) / (INR q - (INR (lengthT l0) - 1) * INR d))%R
      ).
assert
 (INR
   (Proba
     (A ->  Zq) Ef
     (EventInter
       (A ->  Zq) (Eq0 (consT a l0)) (Eventdiff (A ->  Zq) (Eq0 l0)))) *
  / INR (lengthT Ef) <=
  PrCondList (A ->  Zq) Ef (Ev_Evalstozero dec_Evalstozero a) (mapT (Ev_Evalstozero dec_Evalstozero) l0))%R.
assert
 (({ prob (A ->  Zq) Ef (Eventdiff (A ->  Zq) (Eq0 l0)) = 0%R }) +
  ({ prob (A ->  Zq) Ef (Eventdiff (A ->  Zq) (Eq0 l0)) <> 0%R })).
apply Aeq_dec.
case H3.
intros.
assert
 (Proba
   (A ->  Zq) Ef
   (EventInter (A ->  Zq) (Eq0 (consT a l0)) (Eventdiff (A ->  Zq) (Eq0 l0)))
  = 0).
apply inter_0.
unfold prob in e |-.
assert (INR (Proba (A ->  Zq) Ef (Eventdiff (A ->  Zq) (Eq0 l0))) = INR 0).
apply Req_0 with ( b := INR (lengthT Ef) ).
generalize length_Ef;auto with * .
auto with *.
apply INR_eq.
auto with *.
rewrite H4.
rewrite Rmult_0_l.
unfold PrCondList.
apply prob_cond_sup0.
apply length_Ef.
intros.
apply prob_list.
auto with *.
rewrite Rplus_comm.
apply Rplus_le_compat.
apply Rle_trans
     with
      ( r2 :=
      PrCondList (A ->  Zq) Ef (Ev_Evalstozero dec_Evalstozero a) (mapT (Ev_Evalstozero dec_Evalstozero) l0) ).
auto with *.
rewrite <- mult_INR.
generalize (SchwartzExt A n Zq_ring q Q Call Expr transl Fins2list Ef length_Ef dec_Evalstozero schwartz_).
unfold pr_cond; simpl; intros.
apply (H4 a l0 d ).
unfold Exprnon0 in H0 |-; simpl in H0 |-.
intuition.
unfold Exprnon0 in H0 |-; simpl in H0 |-.
intuition.
simpl in H1 |-.
intuition.
simpl in H1 |-.
intuition.
simpl in H2 |-.
rewrite Rdiv_Rmult in H2.
rewrite Rdiv_Rmult.
rewrite mult_INR.
rewrite plus_INR in H2.
rewrite mult_INR in H2.
rewrite Rmult_plus_distr_r in H2.
apply Rle_lt_trans
     with ( r2 := (INR d * / INR q + (INR (lengthT l0) * INR d) * / INR q)%R ).
assert
 (0 + (INR (lengthT l0) * INR d) * / INR q <=
  INR d * / INR q + (INR (lengthT l0) * INR d) * / INR q)%R.
apply Rplus_le_compat.
rewrite <- Rdiv_Rmult.
apply Rle_0.
replace 0%R with (INR 0).
apply le_INR.
auto with *.
auto with *.
apply Q.
auto with *.
rewrite Rplus_0_l in H5.
auto with *.
auto with *.
unfold prob in H |-.
apply Rle_trans
     with
      ( r2 :=
      (INR (Proba (A ->  Zq) Ef (Eq0 l0)) /
       INR (lengthT Ef))%R ).
rewrite <- Rdiv_Rmult.
apply Rle_div.
apply le_inter_r.
apply lt_E.
apply length_Ef.
apply H.
simpl in H0 |-; intuition.
simpl in H1 |-.
intuition.
simpl in H2 |-.
rewrite Rdiv_Rmult in H2.
rewrite Rdiv_Rmult.
rewrite mult_INR.
rewrite plus_INR in H2.
rewrite mult_INR in H2.
rewrite Rmult_plus_distr_r in H2.
apply Rle_lt_trans
     with ( r2 := (INR d * / INR q + (INR (lengthT l0) * INR d) * / INR q)%R ).
assert
 (0 + (INR (lengthT l0) * INR d) * / INR q <=
  INR d * / INR q + (INR (lengthT l0) * INR d) * / INR q)%R.
apply Rplus_le_compat.
rewrite <- Rdiv_Rmult.
apply Rle_0.
replace 0%R with (INR 0).
apply le_INR.
auto with *.
auto with *.
apply Q.
auto with *.
rewrite Rplus_0_l in H4.
auto with *.
auto with *.
assert (lengthT (consT a l0) = S (lengthT l0)).
simpl; auto with *.
rewrite H3.
rewrite S_Rmin.
apply Rle_trans
     with
      ( r2 :=
      (INR d / (INR q - INR (lengthT l0) * INR d) +
       (INR (lengthT l0) * INR d) / (INR q - INR (lengthT l0) * INR d))%R ).
apply Rplus_le_compat.
auto with *.
apply Rle_ge_div.
replace 0%R with (INR 0).
rewrite <- mult_INR.
apply le_INR.
auto with *.
auto with *.
simpl in H2 |-.
apply Rlt_le_trans with ( r2 := (INR q - INR (d + lengthT l0 * d))%R ).
assert (INR (d + lengthT l0 * d) - INR q < 0)%R.
apply Rlt_minus.
apply Rlt_mult.
apply Q.
auto with *.
replace (INR q - INR (d + lengthT l0 * d))%R
     with (- (INR (d + lengthT l0 * d) - INR q))%R.
auto with *.
auto with *.
unfold Rminus.
rewrite plus_INR.
rewrite Rplus_comm with ( r2 := INR (lengthT l0 * d) ).
rewrite Rmult_comm with ( r2 := INR d ).
rewrite mult_INR.
rewrite Ropp_plus_distr.
rewrite Rmult_plus_distr_l.
rewrite Ropp_plus_distr.
rewrite <- Rplus_assoc.
rewrite <- Rplus_assoc.
rewrite Ropp_mult_distr_r_reverse with ( r2 := 1%R ).
rewrite Rmult_1_r.
rewrite Rmult_comm.
rewrite Ropp_involutive.
assert (forall (a c : R), (0 <= c)%R ->  (a - c <= a + c)%R).
apply Rle_min_plus.
unfold Rminus in H4 |-.
apply H4.
replace 0%R with (INR 0).
apply le_INR.
auto with *.
auto with *.
simpl in H2 |-.
apply Rlt_le_trans with ( r2 := (INR q - INR (d + lengthT l0 * d))%R ).
assert (INR (d + lengthT l0 * d) - INR q < 0)%R.
apply Rlt_minus.
apply Rlt_mult.
apply Q.
auto with *.
replace (INR q - INR (d + lengthT l0 * d))%R
     with (- (INR (d + lengthT l0 * d) - INR q))%R.
auto with *.
auto with *.
rewrite plus_INR.
rewrite mult_INR.
unfold Rminus.
rewrite Ropp_plus_distr.
rewrite Rplus_comm with ( r1 := (- INR d)%R ).
rewrite <- Rplus_0_r.
rewrite <- Rplus_assoc.
apply Rplus_le_compat with ( r1 := (INR q + - (INR (lengthT l0) * INR d))%R ).
auto with *.
assert (0 <= INR d)%R.
replace 0%R with (INR 0).
apply le_INR.
auto with *.
auto with *.
auto with *.
auto with *.
rewrite Rmult_comm.
rewrite Rmult_minus_distr_l.
rewrite Rmult_1_r.
unfold Rminus.
rewrite Ropp_plus_distr.
rewrite Ropp_involutive.
rewrite <- Rplus_assoc.
assert
 (INR q + - (INR (lengthT l0) * INR d) <=
  (INR q + - (INR (lengthT l0) * INR d)) + INR d)%R.
rewrite <- Rplus_0_r with ( r := (- (INR (lengthT l0) * INR d))%R ).
rewrite <- Rplus_assoc.
apply Rplus_le_compat.
auto with *.
replace 0%R with (INR 0).
apply le_INR.
auto with *.
auto with *.
rewrite Rmult_comm with ( r1 := INR (lengthT l0) ).
rewrite Rmult_comm.
apply Rle_ge.
auto with *.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite <- Rmult_plus_distr_r.
simpl.
case (lengthT l0).
simpl.
rewrite Rmult_0_l.
rewrite Rmult_1_l.
rewrite Rplus_0_r.
auto with *.
intros.
rewrite Rmult_comm with ( r1 := (INR (S n0) + 1)%R ).
rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rplus_comm.
rewrite Rmult_comm with ( r1 := INR (S n0) ).
auto with *.
Qed.


Lemma InT_ev_impl:
 forall (x : Expr A) (l : listT (Expr A)) (f : A ->  Zq),
 InT x l ->
 Evalstozero transl Fins2list f x ->
  event_pred
   (A ->  Zq)
   (EvUnList
     (A ->  Zq) (mapT (Ev_Evalstozero dec_Evalstozero) l)) f.
induction l.
simpl; intros.
intuition.
simpl; intros.
elim H.
intros h; rewrite h; left; auto.
intro.
right; apply IHl; auto.
Qed.
 

 
Definition list_deg (l : listT (Expr A)) : listT nat :=
   mapT deg_Expr  l.  

Lemma list_deg_app:forall l g:listT (Expr A),
list_deg (appT l g)=appT (list_deg l) (list_deg g).
induction l.
simpl;intros;auto with * .
simpl;intros.
rewrite IHl.
auto with *.
Qed.

Lemma InT_list_deg:
 forall  (p : Expr A) (l : listT (Expr A)),
 InT p l ->  InT (deg_Expr  p) (list_deg l).
induction l.
simpl; intros.
intuition.
simpl; intros.
elim H; intros h.
rewrite h.
left; auto.
right; auto.
Qed.
 
Require Import max.
Lemma inf_deg:
 forall  (p : Expr A) (l : listT (Expr A)),
 InT p l ->  (deg_Expr p <= max_elt 0 (list_deg l)).
induction l.
simpl; intros.
intuition.
simpl; intros.
elim H; intros h.
rewrite h.
apply max_eq.
rewrite max_0_r.
apply InT_max.
apply InT_list_deg.
auto.
Qed.
 

Lemma listPred_:
 forall (l : listT (Expr A)),
  ListPred (fun (p : Expr A) => deg_Expr  p <= max_elt 0 (list_deg l)) l.
intros.
apply listPred_impl.
intros.
apply inf_deg; auto.
Qed.
End col.