val lemma_table_sub_len: len:nat -> table_len:nat -> i:nat{i < table_len} ->
  Lemma (i * len + len <= table_len * len)
let lemma_table_sub_len len table_len i =
  Math.Lemmas.distributivity_add_left i 1 len;
  Math.Lemmas.lemma_mult_le_right len (i + 1) table_len
val lemma_table_sub_len: len:nat -> table_len:nat -> i:nat{i < table_len} ->
  Lemma (i * len + len <= table_len * len)
let lemma_table_sub_len len table_len i =
Math.Lemmas.distributivity_add_left i 1 len;
Math.Lemmas.lemma_mult_le_right len (i + 1) table_len
Hacl.Impl.PrecompTable.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.Definition.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.PrecompTable.fst.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
Hacl.Impl.PrecompTable.fst
Prims.nat Prims.b2t Prims.op_LessThan FStar.Math.Lemmas.lemma_mult_le_right Prims.op_Addition Prims.unit FStar.Math.Lemmas.distributivity_add_left
module Hacl.Impl.PrecompTable

open FStar.Mul

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module B = LowStar.Buffer

module LSeq = Lib.Sequence
module Loops = Lib.LoopCombinators

module BB = Hacl.Bignum.Base
module BD = Hacl.Bignum.Definitions
module PT = Hacl.Spec.PrecompTable
module S = Lib.Exponentiation.Definition

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"

// val lemma_table_sub_len: len:nat -> table_len:nat -> i:nat{i < table_len} ->
//   Lemma (i * len + len <= table_len * len)
val lemma_table_sub_len: len:nat -> table_len:nat -> i:nat{i < table_len} ->
  Lemma (i * len + len <= table_len * len)
len: Prims.nat -> table_len: Prims.nat -> i: Prims.nat{i < table_len}
  -> FStar.Pervasives.Lemma (ensures i * len + len <= table_len * len)