val lemma_pointwise_equal (a b: poly) (pf: (i: int -> Lemma (a.[ i ] == b.[ i ]))) : Lemma (a == b)
let lemma_pointwise_equal (a b:poly) (pf:(i:int -> Lemma (a.[i] == b.[i]))) : Lemma (a == b) =
  FStar.Classical.forall_intro pf;
  lemma_poly_equal_elim a b
val lemma_pointwise_equal (a b: poly) (pf: (i: int -> Lemma (a.[ i ] == b.[ i ]))) : Lemma (a == b)
let lemma_pointwise_equal (a b: poly) (pf: (i: int -> Lemma (a.[ i ] == b.[ i ]))) : Lemma (a == b) =
FStar.Classical.forall_intro pf;
lemma_poly_equal_elim a b
Vale.Math.Poly2.Defs.fst.checked
Vale.Math.Poly2.Defs_s.fst.checked Vale.Def.Prop_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Classical.fsti.checked
Vale.Math.Poly2.Defs.fst
Vale.Math.Poly2.Defs_s.poly Prims.int Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.bool Vale.Math.Poly2.Defs_s.op_String_Access Prims.Nil FStar.Pervasives.pattern Vale.Math.Poly2.Defs.lemma_poly_equal_elim FStar.Classical.forall_intro
module Vale.Math.Poly2.Defs
open FStar.Mul
open Vale.Def.Prop_s
open FStar.Seq
open Vale.Math.Poly2.Defs_s
unfold let max = FStar.Math.Lib.max

#reset-options "--z3rlimit 10"

let poly_equal (a b:poly) : prop0 =
  (forall (i:nat).{:pattern a.[i] \/ b.[i]} a.[i] == b.[i])

unfold let ( =. ) = poly_equal
unfold let ( +. ) = add
unfold let ( *. ) = mul
unfold let ( /. ) = div
unfold let ( %. ) = mod

let lemma_poly_equal_elim (a b:poly) : Lemma
  (requires a =. b)
  (ensures a == b)
  (decreases (length a + length b))
  [SMTPat (poly_equal a b)]
  =
  let len = max (length a) (length b) in
  assert (len > 0 ==> a.[len - 1] == b.[len - 1]);
  assert (length a == length b);
  assert (forall (i:nat).{:pattern (index a i) \/ (index b i)} a.[i] == b.[i]);
  assert (equal a b)
val lemma_pointwise_equal (a b: poly) (pf: (i: int -> Lemma (a.[ i ] == b.[ i ]))) : Lemma (a == b)

    a: Vale.Math.Poly2.Defs_s.poly ->
    b: Vale.Math.Poly2.Defs_s.poly ->
    pf: (i: Prims.int -> FStar.Pervasives.Lemma (ensures a.[ i ] == b.[ i ]))
  -> FStar.Pervasives.Lemma (ensures a == b)