val 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 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_poly_equal_elim (a b: poly)
    : Lemma (requires a =. b)
      (ensures a == b)
      (decreases (length a + length b))
      [SMTPat (poly_equal a b)]
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)
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._assert FStar.Seq.Base.equal Prims.bool Prims.unit Prims.l_Forall Prims.nat Prims.eq2 Vale.Math.Poly2.Defs_s.op_String_Access FStar.Seq.Base.index FStar.Seq.Base.length Prims.l_imp Prims.b2t Prims.op_GreaterThan Prims.op_Subtraction Prims.int Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_Equality Prims.op_LessThan Vale.Math.Poly2.Defs.max Prims.op_Addition Vale.Math.Poly2.Defs.op_Equals_Dot Prims.squash Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Vale.Def.Prop_s.prop0 Vale.Math.Poly2.Defs.poly_equal Prims.Nil
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))
val lemma_poly_equal_elim (a b: poly)
    : Lemma (requires a =. b)
      (ensures a == b)
      (decreases (length a + length b))
      [SMTPat (poly_equal a b)]
a: Vale.Math.Poly2.Defs_s.poly -> b: Vale.Math.Poly2.Defs_s.poly
  -> FStar.Pervasives.Lemma (requires a =. b)
      (ensures a == b)
      (decreases FStar.Seq.Base.length a + FStar.Seq.Base.length b)
      [SMTPat (Vale.Math.Poly2.Defs.poly_equal a b)]