val lemma_degree_is (a:poly) (n:int) : Lemma
  (requires (n >= 0 ==> a.[n]) /\ (forall (i:int).{:pattern a.[i]} i > n ==> not a.[i]))
  (ensures degree a == (if n < 0 then -1 else n))
let lemma_degree_is a n =
  lemma_index a;
  lemma_index_i a n;
  lemma_degree a
val lemma_degree_is (a:poly) (n:int) : Lemma
  (requires (n >= 0 ==> a.[n]) /\ (forall (i:int).{:pattern a.[i]} i > n ==> not a.[i]))
  (ensures degree a == (if n < 0 then -1 else n))
let lemma_degree_is a n =
lemma_index a;
lemma_index_i a n;
lemma_degree a
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 Prims.int Vale.Math.Poly2.lemma_degree Prims.unit Vale.Math.Poly2.lemma_index_i Vale.Math.Poly2.Lemmas.lemma_index
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

let lemma_or_define a b =
  FStar.Classical.forall_intro (lemma_or_define_i a b)

let lemma_or_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun a b -> poly_or a b) lemma_or_define

let lemma_mask_define p n =
  FStar.Classical.forall_intro (lemma_mask_define_i p n);
  ()

let lemma_mask_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun p n -> mask p n) lemma_mask_define

let lemma_reverse_define p n =
  FStar.Classical.forall_intro (lemma_reverse_define_i p n)

let lemma_reverse_define_all () =
  FStar.Classical.forall_intro_2 lemma_reverse_define

let lemma_degree_negative a =
  let f (i:int) : Lemma (not a.[i]) =
    lemma_index_i a i
    in
  FStar.Classical.forall_intro f;
  lemma_zero_define ();
  lemma_equal a zero
val lemma_degree_is (a:poly) (n:int) : Lemma
  (requires (n >= 0 ==> a.[n]) /\ (forall (i:int).{:pattern a.[i]} i > n ==> not a.[i]))
  (ensures degree a == (if n < 0 then -1 else n))
a: Vale.Math.Poly2_s.poly -> n: Prims.int
  -> FStar.Pervasives.Lemma
      (requires
        (n >= 0 ==> a.[ n ]) /\
        (forall (i: Prims.int). {:pattern a.[ i ]} i > n ==> Prims.op_Negation a.[ i ]))
      (ensures
        Vale.Math.Poly2_s.degree a ==
        (match n < 0 with
          | true -> - 1
          | _ -> n))