val to_vec_inc (n k: nat) (a: uint_t k)
    : Lemma (requires (k <= n))
      (ensures
        (pow2 k <= pow2 n /\
          (to_vec #n a) `Seq.equal` ((Seq.create (n - k) false) `Seq.append` (to_vec #k a))))
      (decreases k)
val to_vec_inc (n k: nat) (a: uint_t k)
    : Lemma (requires (k <= n))
      (ensures
        (pow2 k <= pow2 n /\
          (to_vec #n a) `Seq.equal` ((Seq.create (n - k) false) `Seq.append` (to_vec #k a))))
      (decreases k)
let rec to_vec_inc
  (n: nat)
  (k: nat)
  (a: uint_t k)
: Lemma
  (requires (k <= n))
  (ensures (
    pow2 k <= pow2 n /\
    to_vec #n a `Seq.equal` (Seq.create (n - k) false `Seq.append` to_vec #k a)
  ))
  (decreases k)
= if k = 0
  then ()
  else to_vec_inc (n - 1) (k - 1) (a / 2)
module QUIC.UInt
include FStar.UInt
open FStar.Math.Lemmas

#push-options "--z3rlimit 16"

let rec to_vec_prefix
  (n: nat)
  (k: nat)
  (a: uint_t k)
: Lemma
  (requires (k <= n))
  (ensures (
    pow2 k <= pow2 n /\
    to_vec #k a `Seq.equal` Seq.slice (to_vec #n a) (n - k) n
  ))
  (decreases k)
= if k = 0
  then ()
  else to_vec_prefix (n - 1) (k - 1) (a / 2)
/
prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked
QUIC.UInt.fst
n: Prims.nat -> k: Prims.nat -> a: FStar.UInt.uint_t k
  -> FStar.Pervasives.Lemma (requires k <= n)
      (ensures
        Prims.pow2 k <= Prims.pow2 n /\
        FStar.Seq.Base.equal (FStar.UInt.to_vec a)
          (FStar.Seq.Base.append (FStar.Seq.Base.create (n - k) false) (FStar.UInt.to_vec a)))
      (decreases k)
Prims.nat FStar.UInt.uint_t Prims.op_Equality Prims.int Prims.bool QUIC.UInt.to_vec_inc Prims.op_Subtraction Prims.op_Division Prims.unit Prims.b2t Prims.op_LessThanOrEqual Prims.squash Prims.l_and Prims.pow2 FStar.Seq.Base.equal FStar.UInt.to_vec FStar.Seq.Base.append FStar.Seq.Base.create Prims.Nil FStar.Pervasives.pattern
let rec to_vec_inc (n k: nat) (a: uint_t k)
    : Lemma (requires (k <= n))
      (ensures
        (pow2 k <= pow2 n /\
          (to_vec #n a) `Seq.equal` ((Seq.create (n - k) false) `Seq.append` (to_vec #k a))))
      (decreases k) =
  
if k = 0 then () else to_vec_inc (n - 1) (k - 1) (a / 2)