let all_defs =
  poly == D.poly /\
  (forall (p:poly).{:pattern (degree p)} degree p == D.degree (to_poly p)) /\
  zero == of_poly D.zero /\
  one == of_poly D.one /\
  (forall (n:nat).{:pattern (monomial n)} monomial n == of_poly (D.monomial n)) /\
  (forall (p:poly) (n:int).{:pattern (shift p n)} shift p n == of_poly (D.shift (to_poly p) n)) /\
  (forall (p:poly) (n:nat).{:pattern (reverse p n)} reverse p n == of_poly (D.reverse (to_poly p) n)) /\
  (forall (p:poly) (n:int).{:pattern (poly_index p n)} poly_index p n == D.poly_index (to_poly p) n) /\
  (forall (a b:poly).{:pattern (add a b)} add a b == of_poly (D.add (to_poly a) (to_poly b))) /\
  (forall (a b:poly).{:pattern (mul a b)} mul a b == of_poly (D.mul (to_poly a) (to_poly b))) /\
  (forall (a b:poly).{:pattern (div a b)} degree b >= 0 ==> div a b == of_poly (D.div (to_poly a) (to_poly b))) /\
  (forall (a b:poly).{:pattern (mod a b)} degree b >= 0 ==> mod a b == of_poly (D.mod (to_poly a) (to_poly b)))
let all_defs =
poly == D.poly /\ (forall (p: poly). {:pattern (degree p)} degree p == D.degree (to_poly p)) /\
zero == of_poly D.zero /\ one == of_poly D.one /\
(forall (n: nat). {:pattern (monomial n)} monomial n == of_poly (D.monomial n)) /\
(forall (p: poly) (n: int). {:pattern (shift p n)} shift p n == of_poly (D.shift (to_poly p) n)) /\
(forall (p: poly) (n: nat). {:pattern (reverse p n)}
    reverse p n == of_poly (D.reverse (to_poly p) n)) /\
(forall (p: poly) (n: int). {:pattern (poly_index p n)} poly_index p n == D.poly_index (to_poly p) n
) /\
(forall (a: poly) (b: poly). {:pattern (add a b)} add a b == of_poly (D.add (to_poly a) (to_poly b))
) /\
(forall (a: poly) (b: poly). {:pattern (mul a b)} mul a b == of_poly (D.mul (to_poly a) (to_poly b))
) /\
(forall (a: poly) (b: poly). {:pattern (div a b)}
    degree b >= 0 ==> div a b == of_poly (D.div (to_poly a) (to_poly b))) /\
(forall (a: poly) (b: poly). {:pattern (mod a b)}
    degree b >= 0 ==> mod a b == of_poly (D.mod (to_poly a) (to_poly b)))
Vale.Math.Poly2.fst.checked
Vale.Math.Poly2.Defs_s.fst.checked Vale.Math.Poly2.Defs.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked
Vale.Math.Poly2.fst
Prims.l_and Prims.eq2 Vale.Math.Poly2_s.poly Vale.Math.Poly2.Defs_s.poly Prims.l_Forall Prims.int Vale.Math.Poly2_s.degree Vale.Math.Poly2.Defs_s.degree Vale.Math.Poly2_s.to_poly Vale.Math.Poly2_s.zero Vale.Math.Poly2_s.of_poly Vale.Math.Poly2.Defs_s.zero Vale.Math.Poly2_s.one Vale.Math.Poly2.Defs_s.one Prims.nat Vale.Math.Poly2_s.monomial Vale.Math.Poly2.Defs_s.monomial Vale.Math.Poly2_s.shift Vale.Math.Poly2.Defs_s.shift Vale.Math.Poly2_s.reverse Vale.Math.Poly2.Defs_s.reverse Prims.bool Vale.Math.Poly2_s.poly_index Vale.Math.Poly2.Defs_s.poly_index Vale.Math.Poly2_s.add Vale.Math.Poly2.Defs_s.add Vale.Math.Poly2_s.mul Vale.Math.Poly2.Defs_s.mul Prims.l_imp Prims.b2t Prims.op_GreaterThanOrEqual Vale.Math.Poly2_s.div Vale.Math.Poly2.Defs_s.div Vale.Math.Poly2_s.mod Vale.Math.Poly2.Defs_s.mod
module Vale.Math.Poly2
open FStar.Mul
module D = Vale.Math.Poly2.Defs_s
module I = Vale.Math.Poly2.Defs
open FStar.Seq
unfold let max = FStar.Math.Lib.max
val all_defs : Prims.logical
Prims.logical