val lemma_div_sub_small (l n x: nat)
    : Lemma (requires l > 1)
      (ensures
        (n - n % pow2 8) / pow2 (8 `op_Multiply` (l - 1)) == n / pow2 (8 `op_Multiply` (l - 1)))
let lemma_div_sub_small (l:nat) (n:nat) (x:nat)
  : Lemma (requires l > 1)
  (ensures (n - n % pow2 8) / pow2 (8 `op_Multiply` (l-1)) == n / pow2 (8 `op_Multiply` (l-1)))
  =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  lemma_mod_spec n (pow2 8);
  lemma_pow2_div2 n 8 (8*(l-2));
  lemma_pow2_div2 (n - n % pow2 8) 8 (8*(l-2))
val lemma_div_sub_small (l n x: nat)
    : Lemma (requires l > 1)
      (ensures
        (n - n % pow2 8) / pow2 (8 `op_Multiply` (l - 1)) == n / pow2 (8 `op_Multiply` (l - 1)))
let lemma_div_sub_small (l n x: nat)
    : Lemma (requires l > 1)
      (ensures
        (n - n % pow2 8) / pow2 (8 `op_Multiply` (l - 1)) == n / pow2 (8 `op_Multiply` (l - 1))) =
let open FStar.Math.Lemmas in
let open FStar.Mul in
lemma_mod_spec n (pow2 8);
lemma_pow2_div2 n 8 (8 * (l - 2));
lemma_pow2_div2 (n - n % pow2 8) 8 (8 * (l - 2))
QUIC.Spec.Lemmas.fst.checked
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
Prims.nat QUIC.Spec.Lemmas.lemma_pow2_div2 Prims.op_Subtraction Prims.op_Modulus Prims.pow2 FStar.Mul.op_Star Prims.unit FStar.Math.Lemmas.lemma_mod_spec Prims.b2t Prims.op_GreaterThan Prims.squash Prims.eq2 Prims.int Prims.op_Division Prims.op_Multiply Prims.Nil FStar.Pervasives.pattern
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"

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

#pop-options

// We really should have this pattern already...
let lemma_mod0 (x:pos) : Lemma (0 % x == 0)
  [SMTPat (0 % x)] = ()

// Move to FStar.Math.Lemmas?
let lemma_pow2_div (a:nat) (b:nat) (k:nat)
  : Lemma (requires a >= k /\ b >= k)
    (ensures (pow2 a + pow2 b) / pow2 k == pow2 (a - k) + pow2 (b - k))
  =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  pow2_plus k (b - k);
  division_addition_lemma (pow2 a) (pow2 k) (pow2 (b-k));
  pow2_minus b k;
  pow2_minus a k

#restart-solver

let lemma_pow2_div2 (a:nat) (b:nat) (c:nat)
  : Lemma ((a / pow2 b) / pow2 c == a / (pow2 (c + b)))
  =
  let open FStar.Math.Lemmas in
  pow2_plus b c;
  division_multiplication_lemma a (pow2 b) (pow2 c)

let lemma_div_sub_small (l:nat) (n:nat) (x:nat)
  : Lemma (requires l > 1)
  (ensures (n - n % pow2 8) / pow2 (8 `op_Multiply` (l-1)) == n / pow2 (8 `op_Multiply` (l-1)))
val lemma_div_sub_small (l n x: nat)
    : Lemma (requires l > 1)
      (ensures
        (n - n % pow2 8) / pow2 (8 `op_Multiply` (l - 1)) == n / pow2 (8 `op_Multiply` (l - 1)))
l: Prims.nat -> n: Prims.nat -> x: Prims.nat
  -> FStar.Pervasives.Lemma (requires l > 1)
      (ensures (n - n % Prims.pow2 8) / Prims.pow2 (8 * (l - 1)) == n / Prims.pow2 (8 * (l - 1)))