val lemma_index_all (_:unit) : Lemma
  (forall (a:poly) (i:int).{:pattern a.[i]} a.[i] ==> 0 <= i /\ i <= degree a)
let lemma_index_all () =
  FStar.Classical.forall_intro_2 lemma_index_i
val lemma_index_all (_:unit) : Lemma
  (forall (a:poly) (i:int).{:pattern a.[i]} a.[i] ==> 0 <= i /\ i <= degree a)
let lemma_index_all () =
FStar.Classical.forall_intro_2 lemma_index_i
Vale.Math.Poly2.Lemmas.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.List.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Math.Poly2.Lemmas.fst
Prims.unit FStar.Classical.forall_intro_2 Vale.Math.Poly2_s.poly Prims.int Prims.l_imp Prims.b2t Vale.Math.Poly2_s.op_String_Access Prims.l_and Prims.op_LessThanOrEqual Vale.Math.Poly2_s.degree Vale.Math.Poly2.lemma_index_i
module Vale.Math.Poly2.Lemmas
open FStar.Mul

let lemma_pointwise_equal a b pf =
  FStar.Classical.forall_intro pf;
  lemma_equal a b

let lemma_index a =
  FStar.Classical.forall_intro (lemma_index_i a)
val lemma_index_all (_:unit) : Lemma
  (forall (a:poly) (i:int).{:pattern a.[i]} a.[i] ==> 0 <= i /\ i <= degree a)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      forall (a: Vale.Math.Poly2_s.poly) (i: Prims.int). {:pattern a.[ i ]}
        a.[ i ] ==> 0 <= i /\ i <= Vale.Math.Poly2_s.degree a)