let max = FStar.Math.Lib.max
let max =
FStar.Math.Lib.max
Vale.Math.Poly2.fst.checked
Vale.Math.Poly2.Defs_s.fst.checked Vale.Math.Poly2.Defs.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked
Vale.Math.Poly2.fst
FStar.Math.Lib.max
module Vale.Math.Poly2
open FStar.Mul
module D = Vale.Math.Poly2.Defs_s
module I = Vale.Math.Poly2.Defs
val max : x: Prims.int -> y: Prims.int -> z: Prims.int{(x >= y ==> z = x) /\ (x < y ==> z = y)}
x: Prims.int -> y: Prims.int -> z: Prims.int{(x >= y ==> z = x) /\ (x < y ==> z = y)}