Require Import Reals.
Require Import POLY_ax.
Require Import Ring_cat.
Require Import prob.
Require Import Pol_is_ring.
Require Import listT.
Require Import Zq.


Section Schwartz.
Variable q : nat.
Hypothesis Q : (0 < INR q)%R.
 
Definition q_Z := Z_of_nat q.
 
Definition Call: CALL Z.
apply (mk_Call Z (mk_cset Z 0%Z 1%Z (mod_ q_Z) Zplus Zmult Zminus Zopp)).
apply
 (mk_ceq
   Z (mk_cset Z 0%Z 1%Z (mod_ q_Z) Zplus Zmult Zminus Zopp) (mod_refl q)
   (mod_sym (q:=q)) (mod_trans (q:=q)) (Zq_plus_eq (q:=q)) (Zq_mult_eq (q:=q))
   (Zq_plus_opp (q:=q))).
apply (mk_ct Z (mk_cset Z 0%Z 1%Z (mod_ q_Z) Zplus Zmult Zminus Zopp)).
simpl; intros; apply (mod_refl q).
simpl; intros; apply (Zq_plus_sym (q:=q)).
simpl; intros; apply (mod_sym (q:=q)); apply (Zq_plus_ass (q:=q)).
simpl; intros.
case x; simpl; intros; apply (mod_refl q).
simpl; intros; apply (Zqmult_com (q:=q)).
simpl; intros; apply (Zq_mult_ass (q:=q)).
simpl; intros; apply (Zqplus_Zqmult (q:=q)).
simpl; intros.
unfold Zminus; apply (mod_refl q).
simpl; intros; apply (Zq_plus_inv (q:=q)).
Defined.
 
Axiom dec_eq: forall (b a : Z),  ({ mod_ q_Z b a }) + ({ ~ mod_ q_Z b a }).
 
Lemma dec_eqR:
 forall (n : nat) (a : Z) (p : Poly n (R:=Zq_ring q) Call),
  dec_pred (listT Z) (fun (f : listT Z) => ceq Z (COp Z Call) (eval_poly p f) a).
unfold dec_pred.
simpl; intros.
apply dec_eq.
Qed.
Require Import R_lemma.
 
Definition Ev_eq_pol0 (n : nat) (p : Poly n (R:=Zq_ring q) Call) :=
   Build_Event
    _ (fun (f : listT (Zq q)) => mod_ q_Z (eval_poly p f) 0%Z) (dec_eqR n 0%Z p).
 
Lemma eq_p_Pc:
 forall (n : nat) (p : Poly n (R:=Zq_ring q) Call),
 eq_pol p (pol_null n (R:=Zq_ring q) Call) ->
  eq_pol (n:=S n) (R:=Zq_ring q) (Call:=Call) (Pc (Pol Z n) p) (pol_null (S n) (R:=Zq_ring q) Call).
unfold eq_pol; simpl; unfold PolnEq; unfold pol_null; simpl; unfold P0;
 induction n; simpl; intros.
unfold PO; simpl.
apply Eq1_Pc_Pc; auto.
unfold PO; simpl.
apply Eq1_Pc_Pc; auto.
Qed.
 
Lemma not_eq_p_Pc:
 forall (n : nat) (p : Pol Z n),
 ~ eq_pol (n:=S n) (R:=Zq_ring q) (Call:=Call) (Pc (Pol Z n) p) (pol_null (S n) (R:=Zq_ring q) Call) ->
  ~ eq_pol (R:=Zq_ring q) p (pol_null n (R:=Zq_ring q) Call).
intros; generalize (eq_p_Pc n p); intro; intuition.
Qed.
 
Lemma eq_Pc_p:
 forall (n : nat) (p : Pol Z n),
 eq_pol (n:=S n) (R:=Zq_ring q)  (Call:=Call) (Pc (Pol Z n) p) (pol_null (S n) (R:=Zq_ring q) Call) ->
  eq_pol (R:=Zq_ring q) p (pol_null n (R:=Zq_ring q) Call).
unfold eq_pol; simpl; unfold PolnEq; unfold pol_null; simpl; unfold P0; simpl;
 unfold PO; simpl; induction n; simpl; intros.
generalize (Pol1Eq_PC_Ceq Z (COp Z Call)).
simpl; intros h; apply h.
auto.
generalize (Pol1Eq_PC_Ceq (Pol Z (S n)) (COp (Pol Z (S n)) (CPol Z Call (S n)))).
unfold eqC; simpl; unfold ceq; simpl; intros h; apply h.
auto.
Qed.
 
Fixpoint list_Zq (q : nat) : listT (Zq.Zq q) :=
 match q with
   O => nilT _
  | S n' => appT (list_Zq n') (consT (BinInt.Z_of_nat n') (nilT _))
 end.
 
Definition E_Var (n : nat) : listT (listT (Zq q)) :=
   Prod_PS  0%Z n (list_Zq q).
 
Lemma Pr_p_0_not0:
 forall (c : Z) (n : nat),
 ~ mod_ q_Z c 0%Z ->  Proba _ (E_Var n) (Ev_eq_pol0 0 c) = 0.
intros c n; unfold Proba; elim (E_Var n).
simpl; intros; auto.
simpl; intros.
case (dec_eqR 0 0 c a).
simpl; intros; intuition.
simpl; intros.
apply H; auto.
Qed.
 
Lemma Pr_p0_not0:
 forall (n : nat) (c : Z),
 ~ mod_ q_Z c 0%Z ->  (prob _ (E_Var n) (Ev_eq_pol0 0 c) = 0)%R.
intros; unfold prob.
rewrite Pr_p_0_not0.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l; auto.
auto.
Qed.
 
End Schwartz.
Set  Implicit Arguments.
Unset Strict Implicit.
Require Import Logic_Type.
 
Lemma mult_eq_0: forall (a b : nat), a * b = 0 ->  a = 0 \/ b = 0.
induction a; induction b; intuition.
simpl in H |-.
absurd (0 = S (b + a * S b)).
apply O_S.
intuition.
Qed.
 
Lemma not_mult_eq_0: forall (a b : nat), a <> 0 -> b <> 0 ->  (a * b <> 0).
intros.
generalize (mult_eq_0 (a:=a) (b:=b)).
intros; intuition.
Qed.

Lemma lgt_l_n_not0:
 forall (l : listT Z) (n : nat),
 l <> nilT _ ->  (lengthT (Prod_PS 0%Z n l) <> 0).
induction n.
simpl; intros; auto.
simpl; intros.
rewrite lgt_flat_map_cons.
apply not_mult_eq_0.
induction l; simpl; intros; intuition.
simpl in IHn |-.
apply IHn.
auto.
Qed.
 
Lemma lgt_Zq_n_not_0:
 forall (n q : nat),
 q <> 0 ->  (lengthT (Prod_PS 0%Z n (list_Zq q)) <> 0).
intros.
apply lgt_l_n_not0.
induction q.
intuition.
simpl.
apply not_app_cons_nil.
Qed.

Lemma lgt_E_Var: forall (n q : nat), q <> 0 ->  (lengthT (E_Var q (S n)) <> 0).
unfold E_Var; intros.
apply lgt_Zq_n_not_0.
auto.
Qed.
Require Import lgt_filter.
 
Lemma lgt_flat_map_cons:
 forall (A : Event (listT Z)) (l : listT (listT Z)) (a g : listT Z),
 (forall (x : Z),  A (consT x a)) ->
  lengthT
   (filter
     (listT Z) A
     (flatT
       (mapT
         (fun (x : Z) =>
          consT (consT x a) (mapT (fun (y : listT Z) => consT x y) l)) g))) =
  lengthT g +
  lengthT
   (filter
     (listT Z) A
     (flatT (mapT (fun (x : Z) => mapT (fun (y : listT Z) => consT x y) l) g))).
induction g.
simpl; intros.
auto.
simpl; intros.
case (event_dec (listT Z) A (consT a0 a)).
simpl; intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite IHg.
auto with *.
apply H.
simpl; intros.
assert (A (consT a0 a)); auto.
intuition.
Qed.
 
Lemma add_eq: forall (a b c : nat),  (a + b) + c = (a + c) + b.
intros; auto with *.
Qed.
 
Lemma lgt_flat_map_cons_diff:
 forall (n q : nat) (A : Event (listT Z)) (l : listT (listT Z)) (a g : listT Z),
 (forall (x : Z),  ~ A (consT x a)) ->
  lengthT
   (filter
     (listT Z) (Eventdiff _ A)
     (flatT
       (mapT
         (fun (x : Z) =>
          consT (consT x a) (mapT (fun (y : listT Z) => consT x y) l)) g))) =
  lengthT g +
  lengthT
   (filter
     (listT Z) (Eventdiff _ A)
     (flatT (mapT (fun (x : Z) => mapT (fun (y : listT Z) => consT x y) l) g))).
simpl; intros.
apply lgt_flat_map_cons.
simpl; auto.
Qed.
 
Lemma lgt_flat_map_cons_not:
 forall (l : listT (listT Z)) (A : Event (listT Z)) (a g : listT Z),
 (forall (x : Z),  ~ A (consT x a)) ->
  lengthT
   (filter
     (listT Z) A
     (flatT
       (mapT
         (fun (x : Z) =>
          consT (consT x a) (mapT (fun (y : listT Z) => consT x y) l)) g))) =
  lengthT
   (filter
     (listT Z) A
     (flatT (mapT (fun (x : Z) => mapT (fun (y : listT Z) => consT x y) l) g))).
induction g.
simpl; intros.
auto.
simpl; intros.
case (event_dec (listT Z) A (consT a0 a)).
simpl; intros.
assert (~ A (consT a0 a)); auto.
intuition.
simpl; intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite IHg.
auto with *.
apply H.
Qed.
 
Lemma lgt_Zq_1: forall (q : nat),  lengthT (list_Zq q) = q.
simpl.
induction q.
simpl; auto.
simpl; intros.
rewrite lgt_app.
simpl.
auto with *.
Qed.

Lemma Pr_Ev_Pc:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q)  (Call q)),
  Proba _ (E_Var q (S n)) (Ev_eq_pol0 q (S n) (Pc (Pol Z n) p)) =
  q * Proba _ (E_Var q n) (Ev_eq_pol0 q n p).
intros; unfold Proba.
unfold E_Var; simpl.
elim (Prod_PS 0%Z n (list_Zq q)).
simpl; intros; auto.
rewrite flat_map_nil; simpl; auto.
simpl; intros.
case (dec_eqR q n 0 p a).
simpl; intros.
rewrite lgt_flat_map_cons.
rewrite H.
simpl.
change
 (lengthT (list_Zq q) + q * lengthT (filter (listT Z) (Ev_eq_pol0 q n p) l) =
  q * S (lengthT (filter (listT Z) (Ev_eq_pol0 q n p) l))).
rewrite (lgt_Zq_1 q).
rewrite <- mult_n_Sm.
auto with *.
auto.
simpl; intros.
rewrite lgt_flat_map_cons_not.
rewrite H.
auto with *.
auto.
Qed.
 
Lemma lgt_l_Sn:
 forall ( n : nat) (l : listT Z),
  lengthT (Prod_PS 0%Z (S n) l) =
  lengthT l * lengthT (Prod_PS 0%Z n l).
induction l; simpl; intros; auto.
simpl; intros.
rewrite lgt_app.
rewrite lgt_map_cons_.
rewrite listT.lgt_flat_map_cons.
auto.
Qed.
 
Lemma lgt_Zq_Sn:
 forall (q n : nat),
  lengthT (Prod_PS 0%Z (S n) (list_Zq q)) =
  q * lengthT (Prod_PS 0%Z n (list_Zq q)).
intros.
rewrite lgt_l_Sn.
change
 (lengthT (list_Zq q) * lengthT (Prod_PS 0%Z n (list_Zq q)) =
  q * lengthT (Prod_PS 0%Z n (list_Zq q))).
rewrite lgt_Zq_1.
auto.
Qed.
 
Lemma pr_Ev_Pc:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
 INR q <> 0%R ->
  prob _ (E_Var q (S n)) (Ev_eq_pol0 q (S n) (Pc (Pol Z n) p)) =
  prob _ (E_Var q n) (Ev_eq_pol0 q n p).
intros.
unfold prob.
rewrite Pr_Ev_Pc.
unfold E_Var; rewrite lgt_Zq_Sn; auto.
rewrite mult_INR.
rewrite mult_INR.
rewrite Rmult_comm with ( r2 := INR (lengthT (Prod_PS 0%Z n (list_Zq q)))
                        ).
rewrite Rdiv_Rmult_simpl_.
auto.
auto.
generalize (lgt_Zq_n_not_0 (n:=n)(q:=q)).
red; intros.
apply H0.
auto with *.
auto with *.
Qed.
 
Lemma proba_flat_map_nil:
 forall (l : listT Z) (A : Event (listT Z)),
  Proba (listT Z) (flatT (mapT (fun (_ : Z) => nilT (listT Z)) l)) A = 0.
induction l; simpl; intros; auto.
Qed.
 
Lemma le_S:
 forall (a b c d : nat), a <= b + c ->  (S (d + a) <= S (b + (d + c))).
intros.
auto with *.
Qed.
 
Lemma dec_ev_pol:
 forall (n q : nat) (a : Z) (p : Poly n (R:=Zq_ring q) (Call q)) (l : listT Z),
  dec_pred Z (fun (_ : Z) => ceq Z (COp Z (Call q)) (eval_poly p l) a).
unfold dec_pred; simpl; intros.
apply dec_eq.
Qed.
 
Lemma le_plus: forall (a b c d : nat), a <= b + c ->  (d + a <= b + (d + c)).
intros.
auto with *.
Qed.
 
Lemma eq_ev_pol_ev_coef:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)) (a : Z) (a0 : listT Z),
  mod_
   (q_Z q) (ev_pol1 Z (Call q) 0 (eval_coef Z (Call q) n p a0) a)
   (eval_Pol Z (Call q) n (ev_pol1 Z (Call q) n p a) a0).
induction p.
simpl; intros.
unfold eval; simpl; apply mod_refl.
simpl; intros.
apply mod_trans
     with
      (Zplus
        (eval_Pol Z (Call q) n c a0)
        (eval_Pol
          Z (Call q) n (Poln_mulc Z (Call q) n a (ev_pol1 Z (Call q) n p a)) a0)).
apply mod_trans
     with
      (Zplus
        (eval_Pol Z (Call q) n c a0)
        (Zmult a (eval_Pol Z (Call q) n (ev_pol1 Z (Call q) n p a) a0))).
unfold Poln_add; simpl.
unfold Poln_mulc; simpl.
unfold Poln_mul; simpl.
unfold eval; simpl.
apply Zq_plus_eq.
apply mod_refl.
apply Zq_mult_eq.
apply mod_refl.
unfold eval_coef in IHp |-; simpl in IHp |-; unfold eval in IHp |-;
 simpl in IHp |-.
apply IHp.
apply Zq_plus_eq.
apply mod_refl.
apply mod_sym.
apply (ev_pol_mulc_eq Z (Call q) n).
apply mod_sym.
apply (ev_pol_add_eq Z (Call q) n).
Qed.
 
Lemma ev_pol_impl:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)) (a : Z) (a0 : listT Z),
 mod_ (q_Z q) (eval_poly (n:=n) (R:=Zq_ring q) (Call:=Call q) (ev_pol1 Z (Call q) n p a) a0) 0
 /\
 ~ mod_
    (q_Z q)
    (eval_poly
      (n:=n) (R:=Zq_ring q) (Call:=Call q)
      (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)) a0) 0 ->
  mod_ (q_Z q) (ev_pol1 Z (Call q) 0 (eval_coef Z (Call q) n p a0) a) 0 /\
  ~ mod_
     (q_Z q)
     (eval
       Z (Call q) n a0
       (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))) 0.
unfold eval; unfold eval_poly; simpl.
intros.
split.
apply mod_trans with (eval_Pol Z (Call q) n (ev_pol1 Z (Call q) n p a) a0).
apply eq_ev_pol_ev_coef.
intuition.
intuition.
Qed.
 
Lemma ev_pol_impl_:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q)  (Call q)) (a : Z) (a0 : listT Z),
 mod_ (q_Z q) (ev_pol1 Z (Call q) 0 (eval_coef Z (Call q) n p a0) a) 0 /\
 ~ mod_
    (q_Z q)
    (eval
      Z (Call q) n a0
      (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))) 0 ->
  mod_ (q_Z q) (eval_poly (n:=n) (R:=Zq_ring q)  (Call:=Call q) (ev_pol1 Z (Call q) n p a) a0) 0
  /\
  ~ mod_
     (q_Z q)
     (eval_poly
       (n:=n) (R:=Zq_ring q)  (Call:=Call q)
       (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)) a0) 0.
unfold eval; unfold eval_poly; simpl.
intros.
split.
apply mod_trans with (ev_pol1 Z (Call q) 0 (eval_coef Z (Call q) n p a0) a).
apply mod_sym; apply eq_ev_pol_ev_coef.
intuition.
intuition.
Qed.
 
Lemma le_lgt_filt_cons:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)) (a : listT Z)
        (l : listT (listT Z)),
  (lengthT
    (filter
      (listT Z)
      (EventInter
        (listT Z)
        (Build_Event
          (listT (Zq q))
          (fun (f : listT (Zq q)) =>
           mod_ (q_Z q) (eval_poly (n:=S n) (R:=Zq_ring q) (Call:=Call q) p f) 0)
          (dec_eqR q (S n) 0 p))
        (Eventdiff
          (listT Z)
          (Build_Event
            (listT (Zq q))
            (fun (f : listT (Zq q)) =>
             mod_
              (q_Z q)
              (eval_poly
                (n:=S n) (R:=Zq_ring q)  (Call:=Call q)
                (Pc
                  (Pol Z n)
                  (fstT
                    (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))
                f) 0)
            (dec_eqR
              q (S n) 0
              (Pc
                (Pol Z n)
                (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))))))
      (flatT
        (mapT
          (fun (x : Z) =>
           consT (consT x a) (mapT (fun (y : listT Z) => consT x y) l))
          (list_Zq q)))) <=
   lengthT
    (filter
      (listT Z)
      (EventInter
        (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a))
        (Eventdiff
          (listT Z)
          (Ev_eq_pol0
            q 1
            (eval_coef
              Z (Call q) n
              (Pc
                _
                (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))
              a)))) (E_Var q 1)) +
   lengthT
    (filter
      (listT Z)
      (EventInter
        (listT Z) (Ev_eq_pol0 q (S n) p)
        (Eventdiff
          (listT Z)
          (Ev_eq_pol0
            q (S n)
            (Pc
              (Pol Z n)
              (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))))))
      (flatT
        (mapT
          (fun (x : Z) => mapT (fun (y : listT Z) => consT x y) l) (list_Zq q))))).
unfold E_Var; simpl.
intros n q; induction (list_Zq q).
simpl; intros.
auto.
simpl; intros.
change
 (lengthT
   (if event_inter_aux
        (listT Z)
        (Build_Event
          (listT Z)
          (fun (f : listT Z) =>
           mod_
            (q_Z q)
            (eval_poly
              (n:=n) (R:=Zq_ring q) (Call:=Call q) (ev_pol1 Z (Call q) n p (headT 0%Z f))
              (tailT f)) 0) (dec_eqR q (S n) 0 p))
        (Eventdiff
          (listT Z)
          (Build_Event
            (listT Z)
            (fun (f : listT Z) =>
             mod_
              (q_Z q)
              (eval_poly
                (n:=n) (R:=Zq_ring q) (Call:=Call q)
                (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))
                (tailT f)) 0)
            (dec_eqR
              q (S n) 0
              (Pc
                (Pol Z n)
                (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))))))
        (consT a a0)
      then consT
            (consT a a0)
            (filter
              (listT Z)
              (EventInter
                (listT Z)
                (Build_Event
                  (listT Z)
                  (fun (f : listT Z) =>
                   mod_
                    (q_Z q)
                    (eval_poly
                      (n:=n) (R:=Zq_ring q) (Call:=Call q)
                      (ev_pol1 Z (Call q) n p (headT 0%Z f)) (tailT f)) 0)
                  (dec_eqR q (S n) 0 p))
                (Eventdiff
                  (listT Z)
                  (Build_Event
                    (listT Z)
                    (fun (f : listT Z) =>
                     mod_
                      (q_Z q)
                      (eval_poly
                        (n:=n) (R:=Zq_ring q) (Call:=Call q)
                        (fstT
                          (mk_prod
                            (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))
                        (tailT f)) 0)
                    (dec_eqR
                      q (S n) 0
                      (Pc
                        (Pol Z n)
                        (fstT
                          (mk_prod
                            (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))))))
              (appT
                (mapT (fun (y : listT Z) => consT a y) l0)
                (flatT
                  (mapT
                    (fun (x : Z) =>
                     consT
                      (consT x a0) (mapT (fun (y : listT Z) => consT x y) l0)) l))))
      else filter
            (listT Z)
            (EventInter
              (listT Z)
              (Build_Event
                (listT Z)
                (fun (f : listT Z) =>
                 mod_
                  (q_Z q)
                  (eval_poly
                    (n:=n) (R:=Zq_ring q) (Call:=Call q) (ev_pol1 Z (Call q) n p (headT 0%Z f))
                    (tailT f)) 0) (dec_eqR q (S n) 0 p))
              (Eventdiff
                (listT Z)
                (Build_Event
                  (listT Z)
                  (fun (f : listT Z) =>
                   mod_
                    (q_Z q)
                    (eval_poly
                      (n:=n) (R:=Zq_ring q) (Call:=Call q)
                      (fstT
                        (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))
                      (tailT f)) 0)
                  (dec_eqR
                    q (S n) 0
                    (Pc
                      (Pol Z n)
                      (fstT
                        (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))))))
            (appT
              (mapT (fun (y : listT Z) => consT a y) l0)
              (flatT
                (mapT
                  (fun (x : Z) =>
                   consT (consT x a0) (mapT (fun (y : listT Z) => consT x y) l0))
                  l)))) <=
  lengthT
   (if event_inter_aux
        (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a0))
        (Eventdiff
          (listT Z)
          (Ev_eq_pol0
            q 1
            (eval_coef
              Z (Call q) n
              (Pc
                (Pol Z n)
                (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))
              a0))) (consT a (consT 0%Z (nilT Z)))
      then consT
            (consT a (consT 0%Z (nilT Z)))
            (filter
              (listT Z)
              (EventInter
                (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a0))
                (Eventdiff
                  (listT Z)
                  (Ev_eq_pol0
                    q 1
                    (eval_coef
                      Z (Call q) n
                      (Pc
                        (Pol Z n)
                        (fstT
                          (mk_prod
                            (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))
                      a0))))
              (flatT
                (mapT
                  (fun (x : Z) =>
                   consT (consT x (consT 0%Z (nilT Z))) (nilT (listT Z))) l)))
      else filter
            (listT Z)
            (EventInter
              (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a0))
              (Eventdiff
                (listT Z)
                (Ev_eq_pol0
                  q 1
                  (eval_coef
                    Z (Call q) n
                    (Pc
                      (Pol Z n)
                      (fstT
                        (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))
                    a0))))
            (flatT
              (mapT
                (fun (x : Z) =>
                 consT (consT x (consT 0%Z (nilT Z))) (nilT (listT Z))) l))) +
  lengthT
   (filter
     (listT Z)
     (EventInter
       (listT Z) (Ev_eq_pol0 q (S n) p)
       (Eventdiff
         (listT Z)
         (Ev_eq_pol0
           q (S n)
           (Pc
             (Pol Z n)
             (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))))))
     (appT
       (mapT (fun (y : listT Z) => consT a y) l0)
       (flatT (mapT (fun (x : Z) => mapT (fun (y : listT Z) => consT x y) l0) l))))).
case
 (event_inter_aux
   (listT Z)
   (Build_Event
     (listT Z)
     (fun (f : listT Z) =>
      mod_
       (q_Z q)
       (eval_poly
         (n:=n) (R:=Zq_ring q) (Call:=Call q) (ev_pol1 Z (Call q) n p (headT 0%Z f)) (tailT f))
       0) (dec_eqR q (S n) 0 p))
   (Eventdiff
     (listT Z)
     (Build_Event
       (listT Z)
       (fun (f : listT Z) =>
        mod_
         (q_Z q)
         (eval_poly
           (n:=n) (R:=Zq_ring q) (Call:=Call q)
           (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))
           (tailT f)) 0)
       (dec_eqR
         q (S n) 0
         (Pc
           (Pol Z n)
           (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))))))
   (consT a a0)).
case
 (event_inter_aux
   (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a0))
   (Eventdiff
     (listT Z)
     (Ev_eq_pol0
       q 1
       (eval_coef
         Z (Call q) n
         (Pc
           (Pol Z n)
           (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))) a0)))
   (consT a (consT 0%Z (nilT Z)))).
simpl; intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
apply le_S.
apply (IHl p a0 l0).
simpl; intros.
generalize (ev_pol_impl a1).
intro.
intuition.
case
 (event_inter_aux
   (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a0))
   (Eventdiff
     (listT Z)
     (Ev_eq_pol0
       q 1
       (eval_coef
         Z (Call q) n
         (Pc
           (Pol Z n)
           (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))) a0)))
   (consT a (consT 0%Z (nilT Z)))).
simpl; intros.
generalize (ev_pol_impl_ a1).
intro.
intuition.
simpl; intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
apply le_plus.
apply (IHl p a0 l0).
Qed.
 
Definition nb_zeros(n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)): nat.
intros.
case (dec_eq_pol p (pol_null n (R:=Zq_ring q) (Call q))).
intro.
apply 0.
intro.
apply (Proba _ (E_Var q n) (Ev_eq_pol0 q n p)).
Defined.
 
Axiom borne_nb_zeros:
   forall (n q : nat) (p : Poly 1 (R:=Zq_ring q) (Call q)),
   degre Z (Call q) 1 p = n ->  (nb_zeros p <= n).
 
Lemma p0_impl_ev_pol0:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)) (a : listT Z),
 Pol1Eq
  (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p
  (PO (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n))) ->
  Pol1Eq
   Z (mk_cset Z 0%Z 1%Z (mod_ (q_Z q)) Zplus Zmult Zminus Zopp)
   (Pol1map (Pol Z n) Z (eval Z (Call q) n a) p)
   (PO Z (mk_cset Z 0%Z 1%Z (mod_ (q_Z q)) Zplus Zmult Zminus Zopp)).
intros.
generalize (ev_coef_p0 Z (Call q) n p a).
intro.
unfold eval_coef in H0 |-; unfold P0 in H0 |-; simpl in H0 |-.
apply H0.
unfold PolnEq; simpl; auto.
Qed.
 
Lemma le_deg_ev_coef_deg1:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)) (a : listT Z),
  (degre Z (Call q) 1 (eval_coef Z (Call q) n p a) <=
   degre1 (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p).
induction p.
simpl; intros; auto.
simpl; intros.
case
 (dec_EqPol
   Z (mk_cset Z 0%Z 1%Z (mod_ (q_Z q)) Zplus Zmult Zminus Zopp)
   (Pol1map (Pol Z n) Z (eval Z (Call q) n a) p)
   (PO Z (mk_cset Z 0%Z 1%Z (mod_ (q_Z q)) Zplus Zmult Zminus Zopp))).
case
 (dec_EqPol
   (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p
   (PO (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)))).
simpl; intros; auto.
simpl; intros; auto with *.
case
 (dec_EqPol
   (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p
   (PO (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)))).
simpl; intros.
absurd
 (Pol1Eq
   Z (mk_cset Z 0%Z 1%Z (mod_ (q_Z q)) Zplus Zmult Zminus Zopp)
   (Pol1map (Pol Z n) Z (eval Z (Call q) n a) p)
   (PO Z (mk_cset Z 0%Z 1%Z (mod_ (q_Z q)) Zplus Zmult Zminus Zopp))); auto;
 (try apply (p0_impl_ev_pol0 a p0)).
simpl; intros.
unfold degre in IHp |-.
simpl in IHp |-.
unfold eval_coef in IHp |-.
rewrite max.max_0.
auto with *.
Qed.
 
Lemma le_prob_deg_1_var:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)) (a : listT Z),
 ~ eq_pol (n:=1) (R:=Zq_ring q) (eval_coef Z (Call q) n p a) (pol_null 1 (R:=Zq_ring q) (Call q)) ->
  (lengthT
    (filter
      (listT Z)
      (EventInter
        (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a))
        (Eventdiff
          (listT Z)
          (Ev_eq_pol0
            q 1
            (eval_coef
              Z (Call q) n
              (Pc
                _
                (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))
              a)))) (E_Var q 1)) <=
   degre1 (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p).
intros.
generalize borne_nb_zeros.
unfold nb_zeros; unfold Proba.
intro.
apply le_trans
     with
      (lengthT
        (filter
          (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a)) (E_Var q 1))).
generalize le_inter; unfold Proba; intro; auto.
apply le_trans with (degre Z (Call q) 1 (eval_coef Z (Call q) n p a)).
assert
 (degre Z (Call q) 1 (eval_coef Z (Call q) n p a) =
  degre Z (Call q) 1 (eval_coef Z (Call q) n p a)); auto.
auto.
generalize
 (H0
   (degre Z (Call q) 1 (eval_coef Z (Call q) n p a)) q
   (eval_coef Z (Call q) n p a) H1).
case (dec_eq_pol (n:=1) (R:=Zq_ring q) (eval_coef Z (Call q) n p a) (pol_null 1 (R:=Zq_ring q) (Call q))).
simpl; intros.
intuition.
simpl; intros.
apply H2.
apply le_deg_ev_coef_deg1.
Qed.
 
Lemma not_eq_pol_1_var_nil:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)) (a : listT Z),
 ~ mod_
    (q_Z q)
    (eval_poly
      (n:=n) (R:=Zq_ring q) (Call:=Call q)
      (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)) a) 0 ->
  ~ eq_pol
     (n:=1) (R:=Zq_ring q) (Call:=Call q) (eval_coef Z (Call q) n p a) (pol_null 1 (R:=Zq_ring q) (Call q)).
induction p.
unfold eval_poly; simpl; intros.
unfold eval_coef; simpl; intros.
unfold eval; simpl; intros.
generalize (eq_Pc_p q 0 (eval_Pol Z (Call q) n c a)).
unfold eq_pol; simpl; unfold PolnEq; simpl; intro.
red; intro.
absurd (mod_ (q_Z q) (eval_Pol Z (Call q) n c a) 0).
auto.
apply H0; auto.
simpl; intros.
unfold eval_coef; simpl.
unfold eval_coef in IHp |-; simpl in IHp |-.
unfold pol_null; simpl; unfold P0; simpl; unfold PO; simpl.
generalize (Pol1Eq_Pc_PX Z (COp Z (CPol Z (Call q) 0))).
red; intros.
absurd
 (eq_pol
   (n:=1) (R:=Zq_ring q) (Call:=Call q) (Pol1map (Pol Z n) Z (eval Z (Call q) n a) p)
   (pol_null 1 (R:=Zq_ring q) (Call q))).
auto.
unfold eq_pol; simpl; unfold PolnEq; simpl.
apply H0 with ( c := 0%Z ) ( c1 := eval Z (Call q) n a c ).
apply Pol1Eq_sym.
apply CEq.
auto with *.
Qed.
 
Lemma not_eq_pr_eq0:
 forall (q : nat) (A : Event (listT Z)),
 (forall (x : listT Z),  ~ A x) ->  lengthT (filter (listT Z) A (E_Var q 1)) = 0.
intros.
elim E_Var.
simpl; auto.
simpl; intros.
case (event_dec (listT Z) A a).
simpl; auto.
simpl; intros.
absurd (A a).
apply H.
auto.
simpl; intros; auto.
Qed.
 
Lemma le_proba_wo_fst:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
  (Proba
    (listT Z) (E_Var q (S n))
    (EventInter
      (listT Z) (Ev_eq_pol0 q (S n) p)
      (Eventdiff
        (listT Z)
        (Ev_eq_pol0
          q (S n)
          (Pc
            (Pol Z n)
            (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))))))
   <=
   Proba
    (listT Z) (E_Var q n)
    (Eventdiff
      (listT Z)
      (Ev_eq_pol0
        q n (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))) *
   degre1 (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p).
unfold E_Var; simpl; intros.
unfold Proba; simpl.
elim (Prod_PS 0%Z n (list_Zq q)).
simpl; intros.
generalize proba_flat_map_nil; unfold Proba; simpl; intros h; rewrite h.
auto.
intros.
unfold Ev_eq_pol0.
apply le_trans
     with
      (lengthT
        (filter
          (listT Z)
          (EventInter
            (listT Z) (Ev_eq_pol0 q 1 (eval_coef Z (Call q) n p a))
            (Eventdiff
              (listT Z)
              (Ev_eq_pol0
                q 1
                (eval_coef
                  Z (Call q) n
                  (Pc
                    _
                    (fstT
                      (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)))
                  a)))) (E_Var q 1)) +
       lengthT
        (filter
          (listT Z)
          (EventInter
            (listT Z) (Ev_eq_pol0 q (S n) p)
            (Eventdiff
              (listT Z)
              (Ev_eq_pol0
                q (S n)
                (Pc
                  (Pol Z n)
                  (fstT
                    (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))))))
          (flatT
            (mapT
              (fun (x : Z) => mapT (fun (y : listT Z) => consT x y) l)
              (list_Zq q))))).
generalize le_lgt_filt_cons; simpl; intro; auto with *.
simpl.
case
 (event_diff_aux
   (listT Z)
   (Build_Event
     (listT Z)
     (fun (f : listT Z) =>
      mod_
       (q_Z q)
       (eval_poly
         (n:=n) (R:=Zq_ring q) (Call:=Call q)
         (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p)) f) 0)
     (dec_eqR
       q n 0 (fstT (mk_prod (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p))))
   a).
simpl; intro.
apply plus_le_compat.
apply le_prob_deg_1_var.
apply not_eq_pol_1_var_nil; auto.
auto with *.
simpl; intros.
rewrite <- plus_O_n.
apply plus_le_compat.
generalize inter_0; unfold Proba; simpl; intro.
rewrite H0.
auto with *.
apply not_eq_pr_eq0.
auto.
auto.
Qed.
 
Lemma lt_q_0: forall (q : nat), q <> 0 ->  (0 < INR q)%R.
intros.
replace 0%R with (INR 0).
apply lt_INR.
auto with *.
auto with *.
Qed.
 
Lemma eq_pr_diff_Sn_n:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
  q *
  Proba (listT (Zq q)) (E_Var q n) (Eventdiff (listT (Zq q)) (Ev_eq_pol0 q n p))
  =
  Proba
   (listT (Zq q)) (E_Var q (S n))
   (Eventdiff (listT (Zq q)) (Ev_eq_pol0 q (S n) (Pc (Pol Z (pred (S n))) p))).
unfold Proba; unfold E_Var.
simpl; intros.
elim (Prod_PS 0%Z n (list_Zq q)).
simpl; intros.
rewrite flat_map_nil; simpl; auto.
simpl; intros.
case (event_diff_aux (listT Z) (Ev_eq_pol0 q n p) a).
simpl; intros.
rewrite lgt_flat_map_cons.
rewrite <- H.
simpl.
change
 (q * S (lengthT (filter (listT Z) (Eventdiff (listT Z) (Ev_eq_pol0 q n p)) l))
  =
  lengthT (list_Zq q) +
  q * lengthT (filter (listT Z) (Eventdiff (listT Z) (Ev_eq_pol0 q n p)) l)).
rewrite (lgt_Zq_1 q).
rewrite <- mult_n_Sm.
auto with *.
auto.
simpl; intros.
rewrite lgt_flat_map_cons_not.
rewrite <- H.
auto with *.
auto.
Qed.
 
Lemma not_eq_Pr_Sn_n:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
 Proba (listT (Zq q)) (E_Var q n) (Eventdiff (listT (Zq q)) (Ev_eq_pol0 q n p))
 = 0 ->
  Proba
   (listT (Zq q)) (E_Var q (S n))
   (Eventdiff (listT (Zq q)) (Ev_eq_pol0 q (S n) (Pc (Pol Z (pred (S n))) p))) =
  0.
intros.
rewrite <- eq_pr_diff_Sn_n.
rewrite H.
simpl; auto with *.
Qed.
 
Lemma not_eq_pr_Sn_n:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
 INR
  (Proba
    (listT (Zq q)) (E_Var q (S n))
    (Eventdiff (listT (Zq q)) (Ev_eq_pol0 q (S n) (Pc (Pol Z (pred (S n))) p))))
 <> 0%R ->
  (INR
    (Proba
      (listT (Zq q)) (E_Var q n) (Eventdiff (listT (Zq q)) (Ev_eq_pol0 q n p)))
   <> 0%R).
intros.
generalize (not_eq_Pr_Sn_n (n:=n) (q:=q) (p:=p)).
intros.
intro.
apply H.
assert
 (Proba
   (listT (Zq q)) (E_Var q (S n))
   (Eventdiff (listT (Zq q)) (Ev_eq_pol0 q (S n) (Pc (Pol Z (pred (S n))) p))) =
  0).
apply H0; auto.
auto with *.
rewrite H2.
auto with *.
Qed.
 
Lemma le_probcond_t:
 forall (n q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
 q <> 0 ->
  (prob_cond
    _ (E_Var q (S n)) (Ev_eq_pol0 q (S n) p)
    (Eventdiff
      _ (Ev_eq_pol0 q (S n) (Pc _ (fstT (mk_prodn Z (Call q) (S n) p))))) <=
   INR (degre1 (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p) / INR q)%R.
intros.
unfold prob_cond.
assert
 (({
   prob
    _ (E_Var q (S n))
    (Eventdiff
      _ (Ev_eq_pol0 q (S n) (Pc _ (fstT (mk_prodn Z (Call q) (S n) p))))) = 0%R
   }) +
  ({
   prob
    _ (E_Var q (S n))
    (Eventdiff
      _ (Ev_eq_pol0 q (S n) (Pc _ (fstT (mk_prodn Z (Call q) (S n) p))))) <> 0%R
   })).
apply Aeq_dec.
case H0.
intro.
rewrite prob_inter_0.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l; auto with *.
apply Rle_0.
replace 0%R with (INR 0).
apply le_INR.
auto with *.
auto with *.
apply lt_q_0; auto.
unfold E_Var; apply lgt_Zq_n_not_0.
auto with *.
auto.
intro.
unfold prob.
rewrite Rdiv_Rdiv.
apply Rle_trans
     with
      (INR
        (Proba
          _ (E_Var q n)
          (Eventdiff _ (Ev_eq_pol0 q n (fstT (mk_prodn Z (Call q) (S n) p)))) *
         degre1 (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p) /
       INR
        (Proba
          _ (E_Var q (S n))
          (Eventdiff
            _ (Ev_eq_pol0 q (S n) (Pc _ (fstT (mk_prodn Z (Call q) (S n) p)))))))%R.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
apply Rmult_le_compat.
replace 0%R with (INR 0).
apply le_INR.
apply sup_0.
auto with *.
rewrite <- Rmult_1_l.
rewrite <- Rdiv_Rmult.
apply Rle_0.
auto with *.
apply ax5.
auto.
apply le_INR.
simpl.
apply le_proba_wo_fst.
auto with *.
rewrite <- eq_pr_diff_Sn_n.
rewrite mult_INR.
rewrite mult_INR.
rewrite Rdiv_Rmult_simpl_.
auto with *.
apply not_eq_pr_Sn_n.
apply ax1.
auto.
auto with *.
generalize lgt_E_Var.
intro.
apply lt_q_0.
auto with *.
apply ax5.
auto.
Qed.
 
Lemma eq_p_snd:
 forall (n : nat) (q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
 eq_pol
  (n:=pred (S n)) (R:=Zq_ring q) (Call:=Call q) (fstT (mk_prodn Z (Call q) (S n) p))
  (pol_null n (R:=Zq_ring q) (Call q)) ->
  eq_pol (n:=S n) (R:=Zq_ring q) (Call:=Call q) p (sndT (mk_prodn Z (Call q) (S n) p)).
intros.
unfold eq_pol.
apply eq_pol_trans
     with
      (Poln_add
        Z (Call q) (S n)
        (Poln_mulcn
          Z (Call q) (S n) (fstT (mk_prodn Z (Call q) (S n) p))
          (mk_Xtn Z (Call q) (degr1 Z (Call q) (S n) p) (S n)))
        (sndT (mk_prodn Z (Call q) (S n) p))).
generalize (eq_p_mkn Z (Call q) (S n) p).
intro; auto.
apply eq_pol_trans
     with
      (Poln_add
        Z (Call q) (S n) (pol_null (S n) (R:=Zq_ring q) (Call q))
        (sndT (mk_prodn Z (Call q) (S n) p))).
simpl.
apply Polnadd_ext.
unfold PolnEq; simpl.
apply (Pol1_mulc_0 (Pol Z n) (coef1 (Pol Z n) (CPol Z (Call q) n))).
apply Cth.
apply CEq.
auto with *.
apply PolnEq_refl.
unfold PolnEq; simpl.
apply (Polnadd_0_l Z (Call q) (S n)).
Qed.
 
Lemma eq_p_restr_snd:
 forall (n : nat) (q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
 eq_pol
  (n:=pred (S n)) (R:=Zq_ring q) (Call:=Call q) (fstT (mk_prodn Z (Call q) (S n) p))
  (pol_null n (R:=Zq_ring q) (Call q)) ->
  eq_pol
   (n:=S n) (R:=Zq_ring q) (Call:=Call q) p
   (Pc _ (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p)))).
intros.
unfold eq_pol; simpl.
apply (eq_p_restr_snd Z (Call q) n p).
unfold eq_pol in H |-; unfold pol_null in H |-; simpl in H |-.
simpl.
auto with *.
Qed.
 
Lemma eq_deg_deg1:
 forall (n : nat) (q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
 eq_pol
  (n:=pred (S n)) (R:=Zq_ring q) (Call:=Call q) (fstT (mk_prodn Z (Call q) (S n) p))
  (pol_null n (R:=Zq_ring q) (Call q)) ->
  degre Z (Call q) (S n) p =
  degre
   Z (Call q) n (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p))).
intros.
assert
 (degre Z (Call q) (S n) p =
  degre
   Z (Call q) (S n)
   (Pc _ (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p))))).
apply PolnEq_deg_eq.
apply (eq_p_restr_snd (n:= n)(q:=q)); auto.
rewrite H0.
apply degre_Pc_eq.
Qed.
 
Lemma eq_pol_Pr_eq:
 forall (n : nat) (q : nat) (p r : Poly n (R:=Zq_ring q) (Call q)),
 eq_pol (n:=n) (R:=Zq_ring q) (Call:=Call q) p r ->
  Proba _ (E_Var q n) (Ev_eq_pol0 q n p) =
  Proba _ (E_Var q n) (Ev_eq_pol0 q n r).
unfold Proba.
intros; elim (E_Var q n).
simpl; intros; auto.
simpl; intros.
case (dec_eqR q n 0 p a).
case (dec_eqR q n 0 r a).
simpl; intros; auto.
simpl; intros.
absurd (mod_ (q_Z q) (eval_poly (n:=n) (R:=Zq_ring q) (Call:=Call q) r a) 0).
auto.
generalize (eq_pol_ev_eq Z (Call q) n); simpl; unfold PolnEq; simpl; unfold eqC;
 simpl; intros h.
apply mod_trans with (eval_poly (n:=n) (R:=Zq_ring q) (Call:=Call q) p a).
unfold q_Z in h |-.
unfold eval_poly.
simpl; apply h.
apply ceq_sym.
apply CEq.
auto with *.
auto with *.
case (dec_eqR q n 0 r a).
simpl; intros.
absurd (mod_ (q_Z q) (eval_poly (n:=n) (R:=Zq_ring q) (Call:=Call q) p a) 0).
auto.
generalize (eq_pol_ev_eq Z (Call q) n); simpl; unfold PolnEq; simpl; unfold eqC;
 simpl; intros h.
apply mod_trans with (eval_poly (n:=n) (R:=Zq_ring q) (Call:=Call q) r a).
unfold q_Z in h |-.
unfold eval_poly.
simpl; apply h.
auto with *.
auto with *.
simpl; intros; auto.
Qed.
 
Lemma eq_pol_pr_eq:
 forall (n : nat) (q : nat) (p r : Poly n (R:=Zq_ring q) (Call q)),
 eq_pol (n:=n) (R:=Zq_ring q) (Call:=Call q) p r ->
  prob _ (E_Var q n) (Ev_eq_pol0 q n p) = prob _ (E_Var q n) (Ev_eq_pol0 q n r).
intros; unfold prob; rewrite (eq_pol_Pr_eq H); auto.
Qed.
 
Lemma eq_prSn_prn:
 forall (n : nat) (q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
 q <> 0 ->
 eq_pol
  (n:=pred (S n)) (R:=Zq_ring q) (Call:=Call q) (fstT (mk_prodn Z (Call q) (S n) p))
  (pol_null n (R:=Zq_ring q) (Call q)) ->
  prob _ (E_Var q (S n)) (Ev_eq_pol0 q (S n) p) =
  prob
   _ (E_Var q n)
   (Ev_eq_pol0
     q n (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p)))).
intros.
rewrite (eq_pol_pr_eq (eq_p_restr_snd H0)).
apply pr_Ev_Pc.
auto with *.
Qed.
 
Lemma not_eq_rest:
 forall (n : nat) (q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
 eq_pol
  (n:=pred (S n)) (R:=Zq_ring q) (Call:=Call q) (fstT (mk_prodn Z (Call q) (S n) p))
  (pol_null n (R:=Zq_ring q) (Call q)) ->
 ~ eq_pol (n:=S n) (R:=Zq_ring q) (Call:=Call q) p (pol_null (S n) (R:=Zq_ring q) (Call q)) ->
  ~ eq_pol
     (n:=n) (R:=Zq_ring q) (Call:=Call q)
     (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p)))
     (pol_null n (R:=Zq_ring q) (Call q)).
intros.
generalize (eq_p_restr_snd H).
intros.
red; intro.
apply H0.
unfold eq_pol.
apply eq_pol_trans
     with
      (Pc
        (Pol Z n)
        (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p)))).
auto.
apply eq_p_Pc.
auto.
Qed.
 
Lemma le_deg_plus:
 forall (n : nat) (q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
  (degre Z (Call q) n (fstT (mk_prodn Z (Call q) (S n) p)) +
   degre1 (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p <=
   degre Z (Call q) (S n) p).
intros.
apply le_deg_plus.
Qed.
 
Lemma eq_pr_Sn_n:
 forall (n : nat) (q : nat) (p : Poly (S n) (R:=Zq_ring q) (Call q)),
 q <> 0 ->
  prob
   (listT (Zq q)) (E_Var q (S n))
   (Ev_eq_pol0
     q (S n) (Pc (Pol Z (pred (S n))) (fstT (mk_prodn Z (Call q) (S n) p)))) =
  prob
   (listT (Zq q)) (E_Var q n)
   (Ev_eq_pol0 q n (fstT (mk_prodn Z (Call q) (S n) p))).
intros.
simpl.
apply (pr_Ev_Pc (q:=q) (n:=n)).
auto with *.
Qed.
 
Lemma Schwartz:
 forall (n : nat) (q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
 q <> 0 ->
 ~ eq_pol p (pol_null n (R:=Zq_ring q) (Call q)) ->
  (prob _ (E_Var q n) (Ev_eq_pol0 q n p) <= INR (degre Z (Call q) n p) / INR q)%R.
induction n.
unfold eq_pol; unfold pol_null; simpl; unfold PolnEq; unfold P0; simpl; intros.
rewrite Rdiv_Rmult; rewrite Rmult_0_l; rewrite (Pr_p0_not0 q 0); auto with *.
simpl; intros.
case (dec_eq_pol (R:=Zq_ring q) (fstT (mk_prodn Z (Call q) (S n) p)) (pol_null n (R:=Zq_ring q) (Call q))).
intro.
apply Rle_trans
     with
      (prob
        _ (E_Var q n)
        (Ev_eq_pol0
          q n (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p)))))%R.
generalize eq_prSn_prn; simpl; intros h; rewrite h.
auto with *.
auto.
auto.
generalize eq_deg_deg1; simpl; intros h; rewrite h.
apply (IHn q (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p)))).
auto.
apply not_eq_rest; auto.
auto.
auto.
intro.
case (dec_eq_pol (R:=Zq_ring q) (fstT (mk_prodn Z (Call q) (S n) p)) (pol_null n (R:=Zq_ring q) (Call q))).
intro.
apply Rle_trans
     with
      (prob
        _ (E_Var q n)
        (Ev_eq_pol0
          q n (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p)))))%R.
generalize eq_prSn_prn; simpl; intros h; rewrite h.
auto with *.
auto.
auto.
generalize eq_deg_deg1; simpl; intros h; rewrite h.
apply (IHn q (restrict_Pol Z (Call q) n (sndT (mk_prodn Z (Call q) (S n) p)))).
auto.
apply not_eq_rest; auto.
auto.
intro.
apply Rle_trans
     with
      (prob
        _ (E_Var q (S n))
        (Ev_eq_pol0 q (S n) (Pc _ (fstT (mk_prodn Z (Call q) (S n) p)))) +
       prob_cond
        _ (E_Var q (S n)) (Ev_eq_pol0 q (S n) p)
        (Eventdiff
          _ (Ev_eq_pol0 q (S n) (Pc _ (fstT (mk_prodn Z (Call q) (S n) p))))))%R.
apply Rle_pr_pr_cond; auto.
apply lgt_E_Var.
auto.
apply Rle_trans
     with
      ( r2 :=
      (INR (degre Z (Call q) n (fstT (mk_prodn Z (Call q) (S n) p))) / INR q +
       INR (degre1 (Pol Z n) (COp (Pol Z n) (CPol Z (Call q) n)) p) / INR q)%R ).
apply Rplus_le_compat.
rewrite eq_pr_Sn_n.
apply IHn; auto with *.
auto with *.
(**)
apply le_probcond_t.
auto with *.
rewrite <- Rdiv_Rplus_eq.
rewrite <- plus_INR.
apply Rle_div.
generalize le_deg_plus; simpl; intros h; apply h.
apply lt_q_0; auto.
auto with *.
Qed.


 
Lemma dec_eq_nat:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
  dec_pred _ (fun (f : listT (Zq q)) => degre Z (Call q) n p = 0).
unfold dec_pred.
simpl; intros.
apply eq_nat_dec.
Qed.
 
Definition Ev_deg0 (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)) :=
   Build_Event
    _ (fun (f : listT (Zq q)) => degre Z (Call q) n p = 0) (dec_eq_nat p).
 
Axiom pr_inter_pol_deg0:
   forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
    (prob _ (E_Var q n) (EventInter _ (Ev_eq_pol0 q n p) (Ev_deg0 p)) <=
     1 / INR q)%R.
 
Lemma deg0_prob0:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
 degre Z (Call q) n p = 0 ->
  Proba
   _ (E_Var q n) (EventInter _ (Ev_eq_pol0 q n p) (Eventdiff _ (Ev_deg0 p))) = 0.
unfold Proba.
intros.
(* Pr(p=0/\deg p=0)<=Pr(cte=0)=1/q
  deg p=0 => p=cte  *)
elim (E_Var q n).
simpl; intros; auto.
simpl; intros.
case
 (event_inter_aux
   (listT Z) (Ev_eq_pol0 q n p) (Eventdiff (listT Z) (Ev_deg0 (n:=n) (q:=q) p))
   a).
simpl; intros; intuition.
simpl; intros; auto.
Qed.
 
Lemma pr_inter_pol_not_deg0:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
 0 < q ->
  (prob
    _ (E_Var q n) (EventInter _ (Ev_eq_pol0 q n p) (Eventdiff _ (Ev_deg0 p))) <=
   INR (degre Z (Call q) n p) / INR q)%R.
intros.
case (dec_eq_pol p (pol_null n (R:=Zq_ring q) (Call q))).
intro.
assert (degre Z (Call q) n p = 0).
generalize (eq_pol_deg0 (n:=n) (R:=Zq_ring q)) ; simpl.
unfold POLY_ax.degre.
simpl; intros h; apply h; auto.
unfold prob.
rewrite deg0_prob0.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
apply Rle_0.
auto with *.
auto with *.
auto with *.
intros.
apply Rle_trans with (prob _ (E_Var q n) (Ev_eq_pol0 q n p)).
unfold prob.
apply Rle_div.
apply le_inter.
apply lt_q_0.
unfold E_Var; apply lgt_Zq_n_not_0.
auto with *.
assert (q <> 0); auto with *.
apply (Schwartz H0 n0); auto.
Qed.
 
Lemma Schwartz_ext:
 forall (n q : nat) (p : Poly n (R:=Zq_ring q) (Call q)),
 0 < q ->
  (prob _ (E_Var q n) (Ev_eq_pol0 q n p) <=
   (INR (degre Z (Call q) n p) + 1) / INR q)%R.
intros.
unfold prob.
rewrite Prob_plus_op with ( B := Ev_deg0 p ).
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_plus_distr_r.
rewrite plus_INR.
rewrite Rmult_plus_distr_r.
rewrite <- Rdiv_Rmult.
rewrite <- Rdiv_Rmult.
rewrite <- Rdiv_Rmult.
apply Rplus_le_compat.
apply (pr_inter_pol_not_deg0 p); auto.
apply (pr_inter_pol_deg0 p).
Qed.