val lemma_mod_pow2 (a b: nat)
    : Lemma (requires a >= b) (ensures pow2 a % pow2 b == 0) [SMTPat (pow2 a % pow2 b)]
val lemma_mod_pow2 (a b: nat)
    : Lemma (requires a >= b) (ensures pow2 a % pow2 b == 0) [SMTPat (pow2 a % pow2 b)]
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)
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...
/
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
a: Prims.nat -> b: Prims.nat
  -> FStar.Pervasives.Lemma (requires a >= b)
      (ensures Prims.pow2 a % Prims.pow2 b == 0)
      [SMTPat (Prims.pow2 a % Prims.pow2 b)]
Prims.nat FStar.Math.Lemmas.pow2_plus Prims.op_Subtraction Prims.unit FStar.Math.Lemmas.pow2_minus FStar.Math.Lemmas.lemma_div_mod Prims.pow2 Prims.b2t Prims.op_GreaterThanOrEqual Prims.squash Prims.eq2 Prims.int Prims.op_Modulus Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let lemma_mod_pow2 (a 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)