val max (a b: int) : Tot (n: int{n >= a /\ n >= b})
let max (a b:int) : Tot (n:int{n >= a /\ n >= b}) =
  if a > b then a else b
val max (a b: int) : Tot (n: int{n >= a /\ n >= b})
let max (a b: int) : Tot (n: int{n >= a /\ n >= b}) =
if a > b then a else b
QUIC.Spec.Lemmas.fst.checked
QUIC.Spec.Base.fst.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.List.Tot.fst.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked
QUIC.Spec.Lemmas.fst
Prims.int Prims.op_GreaterThan Prims.bool Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual
module QUIC.Spec.Lemmas
open QUIC.Spec.Base

module S = FStar.Seq
module U8 = FStar.UInt8

(* library lemmas *)

let suffix (b:bytes) (n:nat{n <= S.length b}) = S.slice b n (S.length b)
val max (a b: int) : Tot (n: int{n >= a /\ n >= b})
a: Prims.int -> b: Prims.int -> n: Prims.int{n >= a /\ n >= b}