val 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)
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_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)
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
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 Prims.op_LessThan Vale.Bignum.Lemmas.lemma_sum_seq_left_right_rec Prims.op_Subtraction Prims.bool Prims.unit Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.squash Prims.eq2 Prims.op_Addition Vale.Bignum.Defs.sum_seq_left Vale.Bignum.Defs.sum_seq_right Prims.Nil FStar.Pervasives.pattern
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)
val 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)
s: FStar.Seq.Base.seq Prims.int -> i: Prims.nat -> j: Prims.nat -> k: Prims.nat
  -> FStar.Pervasives.Lemma (requires i <= j /\ j <= k /\ k <= FStar.Seq.Base.length s)
      (ensures
        Vale.Bignum.Defs.sum_seq_left s i j + Vale.Bignum.Defs.sum_seq_right s j k ==
        Vale.Bignum.Defs.sum_seq_right s i k)
      (decreases j)