val len_is_w_n_blocksize: w:pos -> blocksize:pos -> n:nat -> Lemma
  (let len = w * n * blocksize in
   len / blocksize = w * n /\ len / (w * blocksize) = n /\
   len % blocksize = 0 /\ len % (w * blocksize) = 0)
let len_is_w_n_blocksize w blocksize n =
  let len = w * n * blocksize in
  Math.Lemmas.cancel_mul_mod (w * n) blocksize;
  //assert (len % blocksize = 0);
  Math.Lemmas.cancel_mul_div (w * n) blocksize;
  //assert (len / blocksize = w * n);

  Math.Lemmas.paren_mul_right n w blocksize;
  Math.Lemmas.cancel_mul_mod n (w * blocksize);
  Math.Lemmas.cancel_mul_div n (w * blocksize)
val len_is_w_n_blocksize: w:pos -> blocksize:pos -> n:nat -> Lemma
  (let len = w * n * blocksize in
   len / blocksize = w * n /\ len / (w * blocksize) = n /\
   len % blocksize = 0 /\ len % (w * blocksize) = 0)
let len_is_w_n_blocksize w blocksize n =
let len = (w * n) * blocksize in
Math.Lemmas.cancel_mul_mod (w * n) blocksize;
Math.Lemmas.cancel_mul_div (w * n) blocksize;
Math.Lemmas.paren_mul_right n w blocksize;
Math.Lemmas.cancel_mul_mod n (w * blocksize);
Math.Lemmas.cancel_mul_div n (w * blocksize)
Lib.Vec.Lemmas.fst.checked
prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Lib.Vec.Lemmas.fst
Prims.pos Prims.nat FStar.Math.Lemmas.cancel_mul_div FStar.Mul.op_Star Prims.unit FStar.Math.Lemmas.cancel_mul_mod FStar.Math.Lemmas.paren_mul_right Prims.int
module Lib.Vec.Lemmas

#set-options ""
#push-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 \
  --using_facts_from '-* +Prims +FStar.Pervasives +FStar.Math.Lemmas +FStar.Seq -FStar.Seq.Properties.slice_slice \
    +Lib.IntTypes +Lib.Sequence +Lib.Sequence.Lemmas +Lib.LoopCombinators +Lib.Vec.Lemmas'"


let rec lemma_repeat_gen_vec w n a a_vec normalize_v f f_v acc_v0 =
  if n = 0 then begin
    Loops.eq_repeat_right 0 n a_vec f_v acc_v0;
    Loops.eq_repeat_right 0 (w * n) a f (normalize_v 0 acc_v0) end
  else begin
    let next_p = Loops.repeat_right 0 (n - 1) a_vec f_v acc_v0 in
    let next_v = Loops.repeat_right 0 (w * (n - 1)) a f (normalize_v 0 acc_v0) in

    calc (==) {
      Loops.repeat_right 0 (w * n) a f (normalize_v 0 acc_v0);
      (==) { Loops.repeat_right_plus 0 (w * (n - 1)) (w * n) a f (normalize_v 0 acc_v0) }
      Loops.repeat_right (w * (n - 1)) (w * n) a f next_v;
      (==) { lemma_repeat_gen_vec w (n - 1) a a_vec normalize_v f f_v acc_v0 }
      Loops.repeat_right (w * (n - 1)) (w * n) a f (normalize_v (n - 1) next_p);
      (==) { }
      normalize_v n (f_v (n - 1) next_p);
      (==) { Loops.unfold_repeat_right 0 n a_vec f_v acc_v0 (n - 1) }
      normalize_v n (Loops.repeat_right 0 n a_vec f_v acc_v0);
    } end


let lemma_repeati_vec #a #a_vec w n normalize_v f f_v acc_v0 =
  lemma_repeat_gen_vec w n (Loops.fixed_a a) (Loops.fixed_a a_vec) (Loops.fixed_i normalize_v) f f_v acc_v0;
  Loops.repeati_def n f_v acc_v0;
  Loops.repeati_def (w * n) f (normalize_v acc_v0)
val len_is_w_n_blocksize: w:pos -> blocksize:pos -> n:nat -> Lemma
  (let len = w * n * blocksize in
   len / blocksize = w * n /\ len / (w * blocksize) = n /\
   len % blocksize = 0 /\ len % (w * blocksize) = 0)
w: Prims.pos -> blocksize: Prims.pos -> n: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      (let len = (w * n) * blocksize in
        len / blocksize = w * n /\ len / (w * blocksize) = n /\ len % blocksize = 0 /\
        len % (w * blocksize) = 0))