val lemma_nat_r432 (r2 r3 r4 c9 c11 d4 d11 t3 r:nat) : Lemma
  (requires
    r2 = c9 % pow2 52 /\ c11 = c9 / pow2 52 + r * pow2 12 * d11 + t3 /\
    r3 = c11 % pow2 52 /\ r4 = c11 / pow2 52 + (d4 % pow2 52) % pow2 48)
  (ensures
    (r4 * pow2 52 + r3) * pow2 52 + r2 =
    c9 + r * d11 * pow2 64 + t3 * pow2 52 + (d4 % pow2 48) * pow2 104)
let lemma_nat_r432 r2 r3 r4 c9 c11 d4 d11 t3 r =
  let k = d4 % pow2 48 in
  calc (==) {
    (r4 * pow2 52 + r3) * pow2 52 + r2;
    (==) { Math.Lemmas.pow2_modulo_modulo_lemma_1 d4 48 52 }
    ((c11 / pow2 52 + k) * pow2 52 + c11 % pow2 52) * pow2 52 + r2;
    (==) { ML.lemma_distr_eucl c11 k }
    (c9 / pow2 52 + r * pow2 12 * d11 + t3 + k * pow2 52) * pow2 52 + c9 % pow2 52;
    (==) { ML.lemma_distr_eucl c9 (r * pow2 12 * d11 + t3 + k * pow2 52) }
    c9 + (r * pow2 12 * d11 + t3 + k * pow2 52) * pow2 52;
    (==) { ML.lemma_distr_pow (r * pow2 12 * d11 + t3) k 52 52 }
    c9 + (r * pow2 12 * d11 + t3) * pow2 52 + k * pow2 104;
    (==) { ML.lemma_swap_mul3 r (pow2 12) d11 }
    c9 + (r * d11 * pow2 12 + t3) * pow2 52 + k * pow2 104;
    (==) { ML.lemma_distr_pow t3 (r * d11) 12 52 }
    c9 + r * d11 * pow2 64 + t3 * pow2 52 + k * pow2 104;
    }
val lemma_nat_r432 (r2 r3 r4 c9 c11 d4 d11 t3 r:nat) : Lemma
  (requires
    r2 = c9 % pow2 52 /\ c11 = c9 / pow2 52 + r * pow2 12 * d11 + t3 /\
    r3 = c11 % pow2 52 /\ r4 = c11 / pow2 52 + (d4 % pow2 52) % pow2 48)
  (ensures
    (r4 * pow2 52 + r3) * pow2 52 + r2 =
    c9 + r * d11 * pow2 64 + t3 * pow2 52 + (d4 % pow2 48) * pow2 104)
let lemma_nat_r432 r2 r3 r4 c9 c11 d4 d11 t3 r =
let k = d4 % pow2 48 in
calc ( == ) {
  (r4 * pow2 52 + r3) * pow2 52 + r2;
  ( == ) { Math.Lemmas.pow2_modulo_modulo_lemma_1 d4 48 52 }
  ((c11 / pow2 52 + k) * pow2 52 + c11 % pow2 52) * pow2 52 + r2;
  ( == ) { ML.lemma_distr_eucl c11 k }
  (c9 / pow2 52 + (r * pow2 12) * d11 + t3 + k * pow2 52) * pow2 52 + c9 % pow2 52;
  ( == ) { ML.lemma_distr_eucl c9 ((r * pow2 12) * d11 + t3 + k * pow2 52) }
  c9 + ((r * pow2 12) * d11 + t3 + k * pow2 52) * pow2 52;
  ( == ) { ML.lemma_distr_pow ((r * pow2 12) * d11 + t3) k 52 52 }
  c9 + ((r * pow2 12) * d11 + t3) * pow2 52 + k * pow2 104;
  ( == ) { ML.lemma_swap_mul3 r (pow2 12) d11 }
  c9 + ((r * d11) * pow2 12 + t3) * pow2 52 + k * pow2 104;
  ( == ) { ML.lemma_distr_pow t3 (r * d11) 12 52 }
  c9 + (r * d11) * pow2 64 + t3 * pow2 52 + k * pow2 104;
}
Hacl.Spec.K256.Field52.Lemmas4.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Spec.K256.Field52.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.K256.Field52.Lemmas4.fst
Prims.nat FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Addition FStar.Mul.op_Star Prims.pow2 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Prims.op_Division Prims.op_Modulus FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.pow2_modulo_modulo_lemma_1 Prims.squash Hacl.Spec.K256.MathLemmas.lemma_distr_eucl Hacl.Spec.K256.MathLemmas.lemma_distr_pow Hacl.Spec.K256.MathLemmas.lemma_swap_mul3
module Hacl.Spec.K256.Field52.Lemmas4

open FStar.Mul
open Lib.IntTypes

module S = Spec.K256

include Hacl.Spec.K256.Field52.Definitions
include Hacl.Spec.K256.Field52

module ML = Hacl.Spec.K256.MathLemmas
module LD = Hacl.Spec.K256.Field52.Definitions.Lemmas

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

val lemma_nat_r432 (r2 r3 r4 c9 c11 d4 d11 t3 r:nat) : Lemma
  (requires
    r2 = c9 % pow2 52 /\ c11 = c9 / pow2 52 + r * pow2 12 * d11 + t3 /\
    r3 = c11 % pow2 52 /\ r4 = c11 / pow2 52 + (d4 % pow2 52) % pow2 48)
  (ensures
    (r4 * pow2 52 + r3) * pow2 52 + r2 =
    c9 + r * d11 * pow2 64 + t3 * pow2 52 + (d4 % pow2 48) * pow2 104)
val lemma_nat_r432 (r2 r3 r4 c9 c11 d4 d11 t3 r:nat) : Lemma
  (requires
    r2 = c9 % pow2 52 /\ c11 = c9 / pow2 52 + r * pow2 12 * d11 + t3 /\
    r3 = c11 % pow2 52 /\ r4 = c11 / pow2 52 + (d4 % pow2 52) % pow2 48)
  (ensures
    (r4 * pow2 52 + r3) * pow2 52 + r2 =
    c9 + r * d11 * pow2 64 + t3 * pow2 52 + (d4 % pow2 48) * pow2 104)

    r2: Prims.nat ->
    r3: Prims.nat ->
    r4: Prims.nat ->
    c9: Prims.nat ->
    c11: Prims.nat ->
    d4: Prims.nat ->
    d11: Prims.nat ->
    t3: Prims.nat ->
    r: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        r2 = c9 % Prims.pow2 52 /\ c11 = c9 / Prims.pow2 52 + (r * Prims.pow2 12) * d11 + t3 /\
        r3 = c11 % Prims.pow2 52 /\ r4 = c11 / Prims.pow2 52 + d4 % Prims.pow2 52 % Prims.pow2 48)
      (ensures
        (r4 * Prims.pow2 52 + r3) * Prims.pow2 52 + r2 =
        c9 + (r * d11) * Prims.pow2 64 + t3 * Prims.pow2 52 + (d4 % Prims.pow2 48) * Prims.pow2 104)