val lemma_sum_seq_left_right (s:seq int) (i j:nat) : Lemma
  (requires i <= j /\ j <= length s)
  (ensures sum_seq_left s i j == sum_seq_right s i j)
let lemma_sum_seq_left_right s i j =
  lemma_sum_seq_left_right_rec s i j j
val lemma_sum_seq_left_right (s:seq int) (i j:nat) : Lemma
  (requires i <= j /\ j <= length s)
  (ensures sum_seq_left s i j == sum_seq_right s i j)
let lemma_sum_seq_left_right s i j =
lemma_sum_seq_left_right_rec s i j j
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
FStar.Seq.Base.seq Prims.int Prims.nat Vale.Bignum.Lemmas.lemma_sum_seq_left_right_rec 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
val lemma_sum_seq_left_right (s:seq int) (i j:nat) : Lemma
  (requires i <= j /\ j <= length s)
  (ensures sum_seq_left s i j == sum_seq_right s i j)
s: FStar.Seq.Base.seq Prims.int -> i: Prims.nat -> j: Prims.nat
  -> FStar.Pervasives.Lemma (requires i <= j /\ j <= FStar.Seq.Base.length s)
      (ensures Vale.Bignum.Defs.sum_seq_left s i j == Vale.Bignum.Defs.sum_seq_right s i j)