val lemma_divrem2 (k a n: nat)
    : Lemma (requires a >= k /\ n < pow2 k)
      (ensures ((pow2 a + n) % pow2 k == n /\ (pow2 a + n) / pow2 k == pow2 (a - k)))
val lemma_divrem2 (k a n: nat)
    : Lemma (requires a >= k /\ n < pow2 k)
      (ensures ((pow2 a + n) % pow2 k == n /\ (pow2 a + n) / pow2 k == pow2 (a - k)))
let lemma_divrem2 (k:nat) (a:nat) (n:nat)
  : Lemma (requires a >= k /\ n < pow2 k)
  (ensures ((pow2 a + n) % pow2 k == n /\ (pow2 a + n) / pow2 k == pow2 (a - k)))
  =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  modulo_distributivity (pow2 a) n (pow2 k);
  small_mod n (pow2 k);
  lemma_div_mod (pow2 a + n) (pow2 k);
  pow2_minus a k
module QUIC.Spec.Lemmas
open QUIC.Spec.Base

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

(* library lemmas *)

let suffix (b:bytes) (n:nat{n <= S.length b}) = S.slice b n (S.length b)

let max (a b:int) : Tot (n:int{n >= a /\ n >= b}) =
  if a > b then a else b // this must exist somewhere...

// Move to FStar.Math.Lemmas?
let lemma_mod_pow2 (a:nat) (b:nat) : Lemma
  (requires a >= b) (ensures pow2 a % pow2 b == 0)
  [SMTPat (pow2 a % pow2 b)]
  =
  let open FStar.Math.Lemmas in
  lemma_div_mod (pow2 a) (pow2 b);
  pow2_minus a b;
  pow2_plus b (a-b)

#push-options "--z3rlimit 16"
/
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
k: Prims.nat -> a: Prims.nat -> n: Prims.nat
  -> FStar.Pervasives.Lemma (requires a >= k /\ n < Prims.pow2 k)
      (ensures
        (Prims.pow2 a + n) % Prims.pow2 k == n /\
        (Prims.pow2 a + n) / Prims.pow2 k == Prims.pow2 (a - k))
Prims.nat FStar.Math.Lemmas.pow2_minus Prims.unit FStar.Math.Lemmas.lemma_div_mod Prims.op_Addition Prims.pow2 FStar.Math.Lemmas.small_mod FStar.Math.Lemmas.modulo_distributivity Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThan Prims.squash Prims.eq2 Prims.int Prims.op_Modulus Prims.op_Division Prims.op_Subtraction Prims.Nil FStar.Pervasives.pattern
let lemma_divrem2 (k a n: nat)
    : Lemma (requires a >= k /\ n < pow2 k)
      (ensures ((pow2 a + n) % pow2 k == n /\ (pow2 a + n) / pow2 k == pow2 (a - k))) =
  
let open FStar.Math.Lemmas in
let open FStar.Mul in
modulo_distributivity (pow2 a) n (pow2 k);
small_mod n (pow2 k);
lemma_div_mod (pow2 a + n) (pow2 k);
pow2_minus a k