val lemma_replace_modulo_bound (a mod_pow new_mod up_pow: nat)
    : Lemma (requires mod_pow < up_pow /\ new_mod < pow2 mod_pow /\ a < pow2 up_pow)
      (ensures replace_modulo' a (pow2 mod_pow) new_mod < pow2 up_pow)
val lemma_replace_modulo_bound (a mod_pow new_mod up_pow: nat)
    : Lemma (requires mod_pow < up_pow /\ new_mod < pow2 mod_pow /\ a < pow2 up_pow)
      (ensures replace_modulo' a (pow2 mod_pow) new_mod < pow2 up_pow)
let lemma_replace_modulo_bound (a mod_pow new_mod up_pow:nat) : Lemma
  (requires
    mod_pow < up_pow /\
    new_mod < pow2 mod_pow /\
    a < pow2 up_pow)
  (ensures replace_modulo' a (pow2 mod_pow) new_mod < pow2 up_pow) =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  let (pmod,umod) = (pow2 mod_pow, pow2 up_pow) in
  lemma_div_mod a pmod;
  multiple_modulo_lemma (a / pmod) pmod;
  lemma_replace_modulo_bound_aux up_pow (a-a%pow2 mod_pow) new_mod mod_pow
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)
  (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)
#pop-options

#push-options "--z3rlimit 1024"
/
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
a: Prims.nat -> mod_pow: Prims.nat -> new_mod: Prims.nat -> up_pow: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires mod_pow < up_pow /\ new_mod < Prims.pow2 mod_pow /\ a < Prims.pow2 up_pow)
      (ensures
        QUIC.Spec.PacketNumber.Lemmas.replace_modulo' a (Prims.pow2 mod_pow) new_mod <
        Prims.pow2 up_pow)
Prims.nat Prims.int Prims.l_and Prims.b2t Prims.op_disEquality Prims.op_GreaterThan Prims.pos QUIC.Spec.PacketNumber.Lemmas.lemma_replace_modulo_bound_aux Prims.op_Subtraction Prims.op_Modulus Prims.pow2 Prims.unit FStar.Math.Lemmas.multiple_modulo_lemma Prims.op_Division FStar.Math.Lemmas.lemma_div_mod FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 Prims.op_LessThan Prims.squash QUIC.Spec.PacketNumber.Lemmas.replace_modulo' Prims.Nil FStar.Pervasives.pattern
let lemma_replace_modulo_bound (a mod_pow new_mod up_pow: nat)
    : Lemma (requires mod_pow < up_pow /\ new_mod < pow2 mod_pow /\ a < pow2 up_pow)
      (ensures replace_modulo' a (pow2 mod_pow) new_mod < pow2 up_pow) =
  
let open FStar.Math.Lemmas in
let open FStar.Mul in
let pmod, umod = (pow2 mod_pow, pow2 up_pow) in
lemma_div_mod a pmod;
multiple_modulo_lemma (a / pmod) pmod;
lemma_replace_modulo_bound_aux up_pow (a - a % pow2 mod_pow) new_mod mod_pow