val usub
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
  (y: uint_t t sec { v y <= v x })
: Tot (z: uint_t t sec { v z == v x - v y })
let usub
  #t #sec x y
= x `sub` y
val usub
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
  (y: uint_t t sec { v y <= v x })
: Tot (z: uint_t t sec { v z == v x - v y })
let usub #t #sec x y =
x `sub` y
QUIC.Secret.Int.fst.checked
QUIC.Secret.Int.Aux.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
QUIC.Secret.Int.fst
Lib.IntTypes.inttype Prims.b2t Lib.IntTypes.unsigned Lib.IntTypes.secrecy_level Lib.IntTypes.uint_t Prims.op_LessThanOrEqual QUIC.Secret.Int.Base.v Lib.IntTypes.sub Prims.eq2 Prims.int Prims.op_Subtraction
module QUIC.Secret.Int
module Aux = QUIC.Secret.Int.Aux

let usub
val usub
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
  (y: uint_t t sec { v y <= v x })
: Tot (z: uint_t t sec { v z == v x - v y })

    x: Lib.IntTypes.uint_t t sec ->
    y: Lib.IntTypes.uint_t t sec {QUIC.Secret.Int.Base.v y <= QUIC.Secret.Int.Base.v x}
  -> z:
    Lib.IntTypes.uint_t t sec
      {QUIC.Secret.Int.Base.v z == QUIC.Secret.Int.Base.v x - QUIC.Secret.Int.Base.v y}