Require Import prob.
Require Import Reals.
Require Import POLY_ax.
Require Import Pol_is_ring.
Require Import Mod_GA.
Require Import listT.

Module Type PS_GA.
Declare Module op:Op_Expr.
Import op.
Import E.

Parameter Ef Eg: listT (Sec ->  Zq).
Parameter length_Ef : lengthT Ef <> 0.
Parameter length_Eg: lengthT Eg <> 0.

Parameter 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. 
End PS_GA.