val swap (a: poly) (n: nat) : poly
let swap (a:poly) (n:nat) : poly =
  shift (mask a n) n +. shift a (-n)
val swap (a: poly) (n: nat) : poly
let swap (a: poly) (n: nat) : poly =
shift (mask a n) n +. shift a (- n)
Vale.Math.Poly2.fsti.checked
Vale.Math.Poly2_s.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2.fsti
Vale.Math.Poly2_s.poly Prims.nat Vale.Math.Poly2.op_Plus_Dot Vale.Math.Poly2_s.shift Vale.Math.Poly2.mask Prims.op_Minus
module Vale.Math.Poly2
open FStar.Mul
open FStar.Seq
open Vale.Math.Poly2_s

// Fundamental lemmas
// (derived lemmas should go in Vale.Math.Poly2.Lemmas_i)

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

let size (a:poly) : int = degree a + 1

val poly_and (a:poly) (b:poly) : poly
val poly_or (a:poly) (b:poly) : poly

// Keep terms up to degree < n, drop terms of degree >= n
val mask (a:poly) (n:nat) : poly
val swap (a: poly) (n: nat) : poly
a: Vale.Math.Poly2_s.poly -> n: Prims.nat -> Vale.Math.Poly2_s.poly