val lemma_i2b_shr (#n:pos) (a:uint_t n) (b:uint_t n) : Lemma
  (b_i2b #n (shift_right #n a b) == b_shr #n (b_i2b a) b)
let lemma_i2b_shr #n a b =
  int2bv_shr #n #a #b #(bvshr #n (int2bv #n a) b) ();
  assert_norm (b_i2b #n (shift_right #n a b) == b_shr #n (b_i2b a) b)
val lemma_i2b_shr (#n:pos) (a:uint_t n) (b:uint_t n) : Lemma
  (b_i2b #n (shift_right #n a b) == b_shr #n (b_i2b a) b)
let lemma_i2b_shr #n a b =
int2bv_shr #n #a #b #(bvshr #n (int2bv #n a) b) ();
assert_norm (b_i2b #n (shift_right #n a b) == b_shr #n (b_i2b a) b)
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 Vale.Math.Bits.b_i2b FStar.UInt.shift_right Vale.Math.Bits.b_shr Prims.unit FStar.BV.int2bv_shr FStar.BV.bvshr FStar.BV.int2bv
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

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))

let lemma_i2b_and #n a b =
  int2bv_logand #n #a #b #(bvand #n (int2bv #n a) (int2bv #n b)) ();
  assert_norm (b_i2b #n (logand #n a b) == b_and #n (b_i2b a) (b_i2b b))

let lemma_i2b_or #n a b =
  int2bv_logor #n #a #b #(bvor #n (int2bv #n a) (int2bv #n b)) ();
  assert_norm (b_i2b #n (logor #n a b) == b_or #n (b_i2b a) (b_i2b b))

let lemma_i2b_xor #n a b =
  int2bv_logxor #n #a #b #(bvxor #n (int2bv #n a) (int2bv #n b)) ();
  assert_norm (b_i2b #n (logxor #n a b) == b_xor #n (b_i2b a) (b_i2b b))

let lemma_i2b_shl #n a b =
  int2bv_shl #n #a #b #(bvshl #n (int2bv #n a) b) ();
  assert_norm (b_i2b #n (shift_left #n a b) == b_shl #n (b_i2b a) b)
val lemma_i2b_shr (#n:pos) (a:uint_t n) (b:uint_t n) : Lemma
  (b_i2b #n (shift_right #n a b) == b_shr #n (b_i2b a) b)
a: FStar.UInt.uint_t n -> b: FStar.UInt.uint_t n
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Math.Bits.b_i2b (FStar.UInt.shift_right a b) ==
      Vale.Math.Bits.b_shr (Vale.Math.Bits.b_i2b a) b)