val suffix : b: QUIC.Spec.Base.bytes -> n: Prims.nat{n <= FStar.Seq.Base.length b}
  -> FStar.Seq.Base.seq QUIC.Spec.Base.byte
let suffix (b:bytes) (n:nat{n <= S.length b}) = S.slice b n (S.length b)
module QUIC.Spec.Lemmas
open QUIC.Spec.Base

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

(* library lemmas *)
/
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
b: QUIC.Spec.Base.bytes -> n: Prims.nat{n <= FStar.Seq.Base.length b}
  -> FStar.Seq.Base.seq QUIC.Spec.Base.byte
QUIC.Spec.Base.bytes Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length QUIC.Spec.Base.byte FStar.Seq.Base.slice FStar.Seq.Base.seq
let suffix (b: bytes) (n: nat{n <= S.length b}) =
  
S.slice b n (S.length b)