val lemma_sum_pow_seq_bound (#n:nat) (s:seq (natN n)) : Lemma
  (ensures 0 <= sum_pow_seq s /\ sum_pow_seq s < pow_int n (length s))
let lemma_sum_pow_seq_bound #n s =
  lemma_sum_pow_seq_bound_rec s (length s)
val lemma_sum_pow_seq_bound (#n:nat) (s:seq (natN n)) : Lemma
  (ensures 0 <= sum_pow_seq s /\ sum_pow_seq s < pow_int n (length s))
let lemma_sum_pow_seq_bound #n s =
lemma_sum_pow_seq_bound_rec s (length s)
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 FStar.Seq.Base.seq Vale.Def.Words_s.natN Vale.Bignum.Lemmas.lemma_sum_pow_seq_bound_rec FStar.Seq.Base.length Prims.unit
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

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

let rec lemma_sum_pow_seq_bound_rec (#n:nat) (s:seq (natN n)) (i:nat{i <= length s}) : Lemma
  (ensures 0 <= sum_pow_seq_left s i /\ sum_pow_seq_left s i < pow_int n i)
  =
  let open FStar.Math.Lemmas in
  if i > 0 then (
    calc (<=) {
      0;
      <= {lemma_sum_pow_seq_bound_rec s (i - 1)}
      sum_pow_seq_left s (i - 1);
      <= {lemma_pow_nat n (i - 1); nat_times_nat_is_nat s.[i - 1] (pow_int n (i - 1))}
      s.[i - 1] * pow_int n (i - 1) + sum_seq_left (pow_seq s) 0 (i - 1);
      == {}
      sum_pow_seq_left s i;
    };
    calc (<=) {
      sum_pow_seq_left s i + 1;
      == {}
      s.[i - 1] * pow_int n (i - 1) + sum_seq_left (pow_seq s) 0 (i - 1) + 1;
      <= {lemma_sum_pow_seq_bound_rec s (i - 1)}
      s.[i - 1] * pow_int n (i - 1) + pow_int n (i - 1);
      <= {lemma_pow_nat n (i - 1); lemma_mult_le_right (pow_int n (i - 1)) s.[i - 1] (n - 1)}
      (n - 1) * pow_int n (i - 1) + pow_int n (i - 1);
      == {}
      pow_int n i;
    }
  )
val lemma_sum_pow_seq_bound (#n:nat) (s:seq (natN n)) : Lemma
  (ensures 0 <= sum_pow_seq s /\ sum_pow_seq s < pow_int n (length s))
s: FStar.Seq.Base.seq (Vale.Def.Words_s.natN n)
  -> FStar.Pervasives.Lemma
    (ensures
      0 <= Vale.Bignum.Defs.sum_pow_seq s /\
      Vale.Bignum.Defs.sum_pow_seq s < Vale.Bignum.Defs.pow_int n (FStar.Seq.Base.length s))