val lemma_replace_modulo_bound_aux (k a b u: nat)
    : Lemma (requires a < pow2 k /\ a % pow2 u == 0 /\ b < pow2 u /\ u < k) (ensures a + b < pow2 k)
let lemma_replace_modulo_bound_aux (k:nat) (a:nat) (b:nat) (u:nat)
  : Lemma (requires a < pow2 k /\ a % pow2 u == 0 /\ b < pow2 u /\ u < k)
  (ensures a + b < pow2 k) =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  lemma_div_mod a (pow2 u);
  assert(a + b == pow2 u * (a / pow2 u) + b);
  lemma_div_plus b (a / pow2 u) (pow2 u);
  small_div b (pow2 u);
  lemma_div_lt_nat a k u;
  assert((a / pow2 u) < pow2 (k-u));
  assert(((a + b) / pow2 u) / pow2 (k-u) < 1);
  division_multiplication_lemma (a+b) (pow2 u) (pow2 (k-u));
  pow2_plus u (k-u)
val lemma_replace_modulo_bound_aux (k a b u: nat)
    : Lemma (requires a < pow2 k /\ a % pow2 u == 0 /\ b < pow2 u /\ u < k) (ensures a + b < pow2 k)
let lemma_replace_modulo_bound_aux (k a b u: nat)
    : Lemma (requires a < pow2 k /\ a % pow2 u == 0 /\ b < pow2 u /\ u < k) (ensures a + b < pow2 k) =
let open FStar.Math.Lemmas in
let open FStar.Mul in
lemma_div_mod a (pow2 u);
assert (a + b == pow2 u * (a / pow2 u) + b);
lemma_div_plus b (a / pow2 u) (pow2 u);
small_div b (pow2 u);
lemma_div_lt_nat a k u;
assert ((a / pow2 u) < pow2 (k - u));
assert (((a + b) / pow2 u) / pow2 (k - u) < 1);
division_multiplication_lemma (a + b) (pow2 u) (pow2 (k - u));
pow2_plus u (k - u)
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 FStar.Math.Lemmas.pow2_plus Prims.op_Subtraction Prims.unit FStar.Math.Lemmas.division_multiplication_lemma Prims.op_Addition Prims.pow2 Prims._assert Prims.b2t Prims.op_LessThan Prims.op_Division FStar.Math.Lemmas.lemma_div_lt_nat FStar.Math.Lemmas.small_div FStar.Math.Lemmas.lemma_div_plus Prims.eq2 Prims.int FStar.Mul.op_Star FStar.Math.Lemmas.lemma_div_mod Prims.l_and Prims.op_Modulus Prims.squash Prims.Nil FStar.Pervasives.pattern
module QUIC.Spec.PacketNumber.Lemmas

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

#push-options "--z3rlimit 256"
let lemma_replace_modulo_bound_aux (k:nat) (a:nat) (b:nat) (u:nat)
  : Lemma (requires a < pow2 k /\ a % pow2 u == 0 /\ b < pow2 u /\ u < k)
val lemma_replace_modulo_bound_aux (k a b u: nat)
    : Lemma (requires a < pow2 k /\ a % pow2 u == 0 /\ b < pow2 u /\ u < k) (ensures a + b < pow2 k)
k: Prims.nat -> a: Prims.nat -> b: Prims.nat -> u10: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires a < Prims.pow2 k /\ a % Prims.pow2 u10 == 0 /\ b < Prims.pow2 u10 /\ u10 < k)
      (ensures a + b < Prims.pow2 k)