val lemma_pow_nat (a:nat) (b:nat) : Lemma (0 <= pow_int a b)
let rec lemma_pow_nat a b =
  if b > 0 then (
    lemma_pow_nat a (b - 1);
    FStar.Math.Lemmas.nat_times_nat_is_nat a (pow_int a (b - 1))
  )
val lemma_pow_nat (a:nat) (b:nat) : Lemma (0 <= pow_int a b)
let rec lemma_pow_nat a b =
if b > 0
then
  (lemma_pow_nat a (b - 1);
    FStar.Math.Lemmas.nat_times_nat_is_nat a (pow_int a (b - 1)))
Vale.Bignum.Lemmas.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Vale.Bignum.Lemmas.fst
Prims.nat Prims.op_GreaterThan FStar.Math.Lemmas.nat_times_nat_is_nat Vale.Bignum.Defs.pow_int Prims.op_Subtraction Prims.unit Vale.Bignum.Lemmas.lemma_pow_nat Prims.bool
module Vale.Bignum.Lemmas
open FStar.Mul

let rec lemma_sum_seq_left_right_rec (s:seq int) (i j k:nat) : Lemma
  (requires i <= j /\ j <= k /\ k <= length s)
  (ensures sum_seq_left s i j + sum_seq_right s j k == sum_seq_right s i k)
  (decreases j)
  =
  if i < j then lemma_sum_seq_left_right_rec s i (j - 1) k

let lemma_sum_seq_left_right s i j =
  lemma_sum_seq_left_right_rec s i j j
val lemma_pow_nat (a:nat) (b:nat) : Lemma (0 <= pow_int a b)
a: Prims.nat -> b: Prims.nat -> FStar.Pervasives.Lemma (ensures 0 <= Vale.Bignum.Defs.pow_int a b)