val lemma_ones_degree (n:nat) : Lemma
  (degree (ones n) == n - 1)
  [SMTPat (degree (ones n))]
let lemma_ones_degree n =
  lemma_ones_define n;
  lemma_degree_is (ones n) (n - 1)
val lemma_ones_degree (n:nat) : Lemma
  (degree (ones n) == n - 1)
  [SMTPat (degree (ones n))]
let lemma_ones_degree n =
lemma_ones_define n;
lemma_degree_is (ones n) (n - 1)
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.nat Vale.Math.Poly2.Lemmas.lemma_degree_is Vale.Math.Poly2.ones Prims.op_Subtraction Prims.unit Vale.Math.Poly2.Lemmas.lemma_ones_define
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

let lemma_degree_is a n =
  lemma_index a;
  lemma_index_i a n;
  lemma_degree a

let lemma_zero_degree =
  lemma_degree zero;
  lemma_zero_define ()

let lemma_one_degree =
  lemma_one_define ();
  lemma_degree_is one 0

let lemma_monomial_degree n =
  lemma_monomial_define n;
  lemma_degree_is (monomial n) n
val lemma_ones_degree (n:nat) : Lemma
  (degree (ones n) == n - 1)
  [SMTPat (degree (ones n))]
n: Prims.nat
  -> FStar.Pervasives.Lemma (ensures Vale.Math.Poly2_s.degree (Vale.Math.Poly2.ones n) == n - 1)
      [SMTPat (Vale.Math.Poly2_s.degree (Vale.Math.Poly2.ones n))]