val lemma_pow2_le (m n:nat) : Lemma (requires m <= n) (ensures pow2 m <= pow2 n)
let lemma_pow2_le m n = FStar.Math.Lemmas.pow2_le_compat n m
val lemma_pow2_le (m n:nat) : Lemma (requires m <= n) (ensures pow2 m <= pow2 n)
let lemma_pow2_le m n =
FStar.Math.Lemmas.pow2_le_compat n m
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.nat FStar.Math.Lemmas.pow2_le_compat Prims.unit
module Vale.Math.Bits
open FStar.Mul
val lemma_pow2_le (m n:nat) : Lemma (requires m <= n) (ensures pow2 m <= pow2 n)
m: Prims.nat -> n: Prims.nat
  -> FStar.Pervasives.Lemma (requires m <= n) (ensures Prims.pow2 m <= Prims.pow2 n)