val lemma_mod_mul_distr (a b:int) (n:pos) : Lemma (a * b % n = (a % n) * (b % n) % n)
let lemma_mod_mul_distr a b n =
  Math.Lemmas.lemma_mod_mul_distr_l a b n;
  Math.Lemmas.lemma_mod_mul_distr_r (a % n) b n
val lemma_mod_mul_distr (a b:int) (n:pos) : Lemma (a * b % n = (a % n) * (b % n) % n)
let lemma_mod_mul_distr a b n =
Math.Lemmas.lemma_mod_mul_distr_l a b n;
Math.Lemmas.lemma_mod_mul_distr_r (a % n) b n
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 Prims.pos FStar.Math.Lemmas.lemma_mod_mul_distr_r Prims.op_Modulus Prims.unit FStar.Math.Lemmas.lemma_mod_mul_distr_l
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)
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_mod_mul_distr (a b:int) (n:pos) : Lemma (a * b % n = (a % n) * (b % n) % n)
val lemma_mod_mul_distr (a b:int) (n:pos) : Lemma (a * b % n = (a % n) * (b % n) % n)
a: Prims.int -> b: Prims.int -> n: Prims.pos
  -> FStar.Pervasives.Lemma (ensures a * b % n = (a % n) * (b % n) % n)