val lemma_i2b_uext (#n m:pos) (a:uint_t n) : Lemma
  (b_i2b (uext #n #m a) == b_uext #n #m (b_i2b #n a))
let lemma_i2b_uext #n m a =
  Vale.Lib.Bv_s.int2bv_uext #n #m a (uext #n #m a);
  assert_norm (b_i2b (uext #n #m a) == b_uext #n #m (b_i2b #n a))
val lemma_i2b_uext (#n m:pos) (a:uint_t n) : Lemma
  (b_i2b (uext #n #m a) == b_uext #n #m (b_i2b #n a))
let lemma_i2b_uext #n m a =
Vale.Lib.Bv_s.int2bv_uext #n #m a (uext #n #m a);
assert_norm (b_i2b (uext #n #m a) == b_uext #n #m (b_i2b #n a))
Vale.Math.Bits.fst.checked
Vale.Lib.Bv_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Vale.Math.Bits.fst
Prims.pos FStar.UInt.uint_t FStar.Pervasives.assert_norm Prims.eq2 FStar.BV.bv_t Prims.op_Addition Vale.Math.Bits.b_i2b Vale.Math.Bits.uext Vale.Math.Bits.b_uext Prims.unit Vale.Lib.Bv_s.int2bv_uext
module Vale.Math.Bits
open FStar.Mul

let lemma_pow2_le m n = FStar.Math.Lemmas.pow2_le_compat n m

let lemma_i2b_eq #n a b =
  assert_norm (b_i2b a == b_i2b b ==> int2bv a == int2bv b);
  int2bv_lemma_2 #n a b
val lemma_i2b_uext (#n m:pos) (a:uint_t n) : Lemma
  (b_i2b (uext #n #m a) == b_uext #n #m (b_i2b #n a))
m: Prims.pos -> a: FStar.UInt.uint_t n
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Math.Bits.b_i2b (Vale.Math.Bits.uext a) == Vale.Math.Bits.b_uext (Vale.Math.Bits.b_i2b a)
    )