val lemma_or_define (a b:poly) : Lemma
  (forall (i:int).{:pattern (poly_or a b).[i] \/ a.[i] \/ b.[i]} (poly_or a b).[i] == (a.[i] || b.[i]))
let lemma_or_define a b =
  FStar.Classical.forall_intro (lemma_or_define_i a b)
val lemma_or_define (a b:poly) : Lemma
  (forall (i:int).{:pattern (poly_or a b).[i] \/ a.[i] \/ b.[i]} (poly_or a b).[i] == (a.[i] || b.[i]))
let lemma_or_define a b =
FStar.Classical.forall_intro (lemma_or_define_i a b)
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
Vale.Math.Poly2_s.poly FStar.Classical.forall_intro Prims.int Prims.eq2 Prims.bool Vale.Math.Poly2_s.op_String_Access Vale.Math.Poly2.poly_or Prims.op_BarBar Vale.Math.Poly2.lemma_or_define_i Prims.unit
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)

let lemma_index_all () =
  FStar.Classical.forall_intro_2 lemma_index_i

let lemma_zero_define () =
  FStar.Classical.forall_intro lemma_zero_define_i

let lemma_one_define () =
  FStar.Classical.forall_intro lemma_one_define_i

let lemma_monomial_define n =
  FStar.Classical.forall_intro (lemma_monomial_define_i n)

let lemma_monomial_define_all () =
  FStar.Classical.forall_intro_with_pat (fun n -> monomial n) lemma_monomial_define

let lemma_ones_define n =
  FStar.Classical.forall_intro (lemma_ones_define_i n)

let lemma_ones_define_all () =
  FStar.Classical.forall_intro_with_pat (fun n -> ones n) lemma_ones_define

let lemma_shift_define p n =
  FStar.Classical.forall_intro (lemma_shift_define_i p n)

let lemma_shift_define_forward p n =
  lemma_shift_define p n

let lemma_shift_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun p n -> shift p n) lemma_shift_define

let lemma_and_define a b =
  FStar.Classical.forall_intro (lemma_and_define_i a b)

let lemma_and_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun a b -> poly_and a b) lemma_and_define
val lemma_or_define (a b:poly) : Lemma
  (forall (i:int).{:pattern (poly_or a b).[i] \/ a.[i] \/ b.[i]} (poly_or a b).[i] == (a.[i] || b.[i]))
a: Vale.Math.Poly2_s.poly -> b: Vale.Math.Poly2_s.poly
  -> FStar.Pervasives.Lemma
    (ensures
      forall (i: Prims.int). {:pattern (Vale.Math.Poly2.poly_or a b).[ i ]\/a.[ i ]\/b.[ i ]}
        (Vale.Math.Poly2.poly_or a b).[ i ] == (a.[ i ] || b.[ i ]))