val lemma_swap_mul3 (a b c:int) : Lemma (a * b * c == a * c * b)
let lemma_swap_mul3 a b c =
  calc (==) {
    a * b * c;
    (==) { Math.Lemmas.paren_mul_right a b c }
    a * (b * c);
    (==) { Math.Lemmas.swap_mul b c }
    a * (c * b);
    (==) { Math.Lemmas.paren_mul_right a c b }
    a * c * b;
  }
val lemma_swap_mul3 (a b c:int) : Lemma (a * b * c == a * c * b)
let lemma_swap_mul3 a b c =
calc ( == ) {
  (a * b) * c;
  ( == ) { Math.Lemmas.paren_mul_right a b c }
  a * (b * c);
  ( == ) { Math.Lemmas.swap_mul b c }
  a * (c * b);
  ( == ) { Math.Lemmas.paren_mul_right a c b }
  (a * c) * b;
}
Hacl.Spec.K256.MathLemmas.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.K256.MathLemmas.fst
Prims.int FStar.Calc.calc_finish Prims.eq2 FStar.Mul.op_Star Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.paren_mul_right Prims.squash FStar.Math.Lemmas.swap_mul
module Hacl.Spec.K256.MathLemmas

open FStar.Mul

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

val lemma_swap_mul3 (a b c:int) : Lemma (a * b * c == a * c * b)
val lemma_swap_mul3 (a b c:int) : Lemma (a * b * c == a * c * b)
a: Prims.int -> b: Prims.int -> c: Prims.int
  -> FStar.Pervasives.Lemma (ensures (a * b) * c == (a * c) * b)