val lemma_distr_eucl_mul_add (r a c:int) (b:pos) : Lemma (r * (a % b) + r * (a / b + c) * b = r * a + r * c * b)
let lemma_distr_eucl_mul_add r a c b =
  calc (==) {
    r * (a % b) + r * (a / b + c) * b;
    (==) { Math.Lemmas.paren_mul_right r (a / b + c) b }
    r * (a % b) + r * ((a / b + c) * b);
    (==) { Math.Lemmas.distributivity_add_left (a / b) c b }
    r * (a % b) + r * ((a / b * b) + c * b);
    (==) { Math.Lemmas.distributivity_add_right r (a / b * b) (c * b) }
    r * (a % b) + r * (a / b * b) + r * (c * b);
    (==) { Math.Lemmas.paren_mul_right r (a / b) b; Math.Lemmas.paren_mul_right r c b }
    r * (a % b) + r * (a / b) * b + r * c * b;
    (==) { lemma_distr_eucl_mul r a b }
    r * a + r * c * b;
  }
val lemma_distr_eucl_mul_add (r a c:int) (b:pos) : Lemma (r * (a % b) + r * (a / b + c) * b = r * a + r * c * b)
let lemma_distr_eucl_mul_add r a c b =
calc ( == ) {
  r * (a % b) + (r * (a / b + c)) * b;
  ( == ) { Math.Lemmas.paren_mul_right r (a / b + c) b }
  r * (a % b) + r * ((a / b + c) * b);
  ( == ) { Math.Lemmas.distributivity_add_left (a / b) c b }
  r * (a % b) + r * (((a / b) * b) + c * b);
  ( == ) { Math.Lemmas.distributivity_add_right r ((a / b) * b) (c * b) }
  r * (a % b) + r * ((a / b) * b) + r * (c * b);
  ( == ) { (Math.Lemmas.paren_mul_right r (a / b) b;
    Math.Lemmas.paren_mul_right r c b) }
  r * (a % b) + (r * (a / b)) * b + (r * c) * b;
  ( == ) { lemma_distr_eucl_mul r a b }
  r * a + (r * 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 Prims.pos FStar.Calc.calc_finish Prims.eq2 Prims.op_Addition FStar.Mul.op_Star Prims.op_Modulus Prims.op_Division 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.distributivity_add_left FStar.Math.Lemmas.distributivity_add_right Hacl.Spec.K256.MathLemmas.lemma_distr_eucl_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)
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)
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_sub_distr (a b:int) (n:pos) : Lemma ((a - b) % n = (a % n - b % n) % n)
let lemma_mod_sub_distr a b n =
  Math.Lemmas.lemma_mod_plus_distr_l a (- b) n;
  Math.Lemmas.lemma_mod_sub_distr (a % n) b n


val lemma_ab_le_cd (a b c d:nat) : Lemma
  (requires a <= c /\ b <= d)
  (ensures a * b <= c * d)
let lemma_ab_le_cd a b c d =
  Math.Lemmas.lemma_mult_le_left a b d;
  Math.Lemmas.lemma_mult_le_right d a c


val lemma_ab_lt_cd (a b c d:pos) : Lemma
  (requires a < c /\ b < d)
  (ensures a * b < c * d)
let lemma_ab_lt_cd a b c d =
  Math.Lemmas.lemma_mult_lt_left a b d;
  Math.Lemmas.lemma_mult_lt_right d a c


val lemma_bound_mul64_wide (ma mb:nat) (mma mmb:nat) (a b:nat) : Lemma
  (requires a <= ma * mma /\ b <= mb * mmb)
  (ensures  a * b <= ma * mb * (mma * mmb))

let lemma_bound_mul64_wide ma mb mma mmb a b =
  calc (<=) {
    a * b;
    (<=) { lemma_ab_le_cd a b (ma * mma) (mb * mmb) }
    (ma * mma) * (mb * mmb);
    (==) { Math.Lemmas.paren_mul_right ma mma (mb * mmb) }
    ma * (mma * (mb * mmb));
    (==) {
      Math.Lemmas.paren_mul_right mma mb mmb;
      Math.Lemmas.swap_mul mma mb;
      Math.Lemmas.paren_mul_right mb mma mmb }
    ma * (mb * (mma * mmb));
    (==) { Math.Lemmas.paren_mul_right ma mb (mma * mmb) }
    ma * mb * (mma * mmb);
  }


val lemma_distr_pow (a b:int) (c d:nat) : Lemma ((a + b * pow2 c) * pow2 d = a * pow2 d + b * pow2 (c + d))
let lemma_distr_pow a b c d =
  calc (==) {
    (a + b * pow2 c) * pow2 d;
    (==) { Math.Lemmas.distributivity_add_left a (b * pow2 c) (pow2 d) }
    a * pow2 d + b * pow2 c * pow2 d;
    (==) { Math.Lemmas.paren_mul_right b (pow2 c) (pow2 d); Math.Lemmas.pow2_plus c d }
    a * pow2 d + b * pow2 (c + d);
  }


val lemma_distr_pow_pow (a:int) (b:nat) (c:int) (d e:nat) :
  Lemma ((a * pow2 b + c * pow2 d) * pow2 e = a * pow2 (b + e) + c * pow2 (d + e))
let lemma_distr_pow_pow a b c d e =
  calc (==) {
    (a * pow2 b + c * pow2 d) * pow2 e;
    (==) { lemma_distr_pow (a * pow2 b) c d e }
    a * pow2 b * pow2 e + c * pow2 (d + e);
    (==) { Math.Lemmas.paren_mul_right a (pow2 b) (pow2 e); Math.Lemmas.pow2_plus b e }
    a * pow2 (b + e) + c * pow2 (d + e);
  }


val lemma_distr_eucl_mul (r a:int) (b:pos) : Lemma (r * (a % b) + r * (a / b) * b = r * a)
let lemma_distr_eucl_mul r a b =
  calc (==) {
    r * (a % b) + r * (a / b) * b;
    (==) { Math.Lemmas.paren_mul_right r (a / b) b }
    r * (a % b) + r * ((a / b) * b);
    (==) { Math.Lemmas.distributivity_add_right r (a % b) (a / b * b) }
    r * (a % b + a / b * b);
    (==) { Math.Lemmas.euclidean_division_definition a b }
    r * a;
  }


val lemma_distr_eucl_mul_add (r a c:int) (b:pos) : Lemma (r * (a % b) + r * (a / b + c) * b = r * a + r * c * b)
val lemma_distr_eucl_mul_add (r a c:int) (b:pos) : Lemma (r * (a % b) + r * (a / b + c) * b = r * a + r * c * b)
r: Prims.int -> a: Prims.int -> c: Prims.int -> b: Prims.pos
  -> FStar.Pervasives.Lemma (ensures r * (a % b) + (r * (a / b + c)) * b = r * a + (r * c) * b)