val size (a: poly) : int
let size (a:poly) : int = degree a + 1
val size (a: poly) : int
let size (a: poly) : int =
degree a + 1
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.op_Addition Vale.Math.Poly2_s.degree Prims.int
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
val size (a: poly) : int
a: Vale.Math.Poly2_s.poly -> Prims.int