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_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);
}
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.nat FStar.Calc.calc_finish Prims.int Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Prims.Cons FStar.Preorder.relation Prims.eq2 Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Hacl.Spec.K256.MathLemmas.lemma_ab_le_cd Prims.squash FStar.Math.Lemmas.paren_mul_right 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)
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))
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))
ma: Prims.nat -> mb: Prims.nat -> mma: Prims.nat -> mmb: Prims.nat -> a: Prims.nat -> b: Prims.nat
  -> FStar.Pervasives.Lemma (requires a <= ma * mma /\ b <= mb * mmb)
      (ensures a * b <= (ma * mb) * (mma * mmb))