val replace_modulo' (a b new_mod: nat)
    : Pure nat
      (requires b > 0 /\ new_mod < b)
      (ensures fun res -> res % b = new_mod /\ res / b = a / b)
let replace_modulo' (a b new_mod:nat) : Pure nat
  (requires b > 0 /\ new_mod < b)
  (ensures fun res -> res % b = new_mod /\ res / b = a / b) =
  let open FStar.Math.Lemmas in
  let res = a - a%b + new_mod in
  lemma_mod_plus new_mod (a/b) b;
  small_mod new_mod b;
  res
val replace_modulo' (a b new_mod: nat)
    : Pure nat
      (requires b > 0 /\ new_mod < b)
      (ensures fun res -> res % b = new_mod /\ res / b = a / b)
let replace_modulo' (a b new_mod: nat)
    : Pure nat
      (requires b > 0 /\ new_mod < b)
      (ensures fun res -> res % b = new_mod /\ res / b = a / b) =
let open FStar.Math.Lemmas in
let res = a - a % b + new_mod in
lemma_mod_plus new_mod (a / b) b;
small_mod new_mod b;
res
QUIC.Spec.PacketNumber.Lemmas.fst.checked
QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Ghost.fsti.checked
QUIC.Spec.PacketNumber.Lemmas.fst
Prims.nat Prims.unit FStar.Math.Lemmas.small_mod FStar.Math.Lemmas.lemma_mod_plus Prims.op_Division Prims.int Prims.op_Addition Prims.op_Subtraction Prims.op_Modulus Prims.l_and Prims.b2t Prims.op_GreaterThan Prims.op_LessThan Prims.op_Equality
module QUIC.Spec.PacketNumber.Lemmas

let replace_modulo' (a b new_mod:nat) : Pure nat
  (requires b > 0 /\ new_mod < b)
val replace_modulo' (a b new_mod: nat)
    : Pure nat
      (requires b > 0 /\ new_mod < b)
      (ensures fun res -> res % b = new_mod /\ res / b = a / b)
a: Prims.nat -> b: Prims.nat -> new_mod: Prims.nat -> Prims.Pure Prims.nat