val fsub5:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> f2:felem5{felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (9, 10, 9, 9, 9) /\
    feval out == fsub (feval f1) (feval f2)}
let fsub5 (f10, f11, f12, f13, f14) (f20, f21, f22, f23, f24) =
  //assert_norm (0x3fffffffffff68 == pow2 54 - 152);
  //assert_norm (0x3ffffffffffff8 == pow2 54 - 8);
  let (t0, t1, t2, t3, t4) = fadd_zero (f10, f11, f12, f13, f14) in
  let o0 = t0 -! f20 in
  let o1 = t1 -! f21 in
  let o2 = t2 -! f22 in
  let o3 = t3 -! f23 in
  let o4 = t4 -! f24 in
  let out = (o0, o1, o2, o3, o4) in
  FStar.Math.Lemmas.lemma_mod_plus_distr_l
    (as_nat5 (t0, t1, t2, t3, t4)) (- as_nat5 (f20, f21, f22, f23, f24)) prime;
  lemma_mod_sub_distr ((as_nat5 (t0, t1, t2, t3, t4)) % prime) (as_nat5 (f20, f21, f22, f23, f24)) prime;
  out
val fsub5:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> f2:felem5{felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (9, 10, 9, 9, 9) /\
    feval out == fsub (feval f1) (feval f2)}
let fsub5 (f10, f11, f12, f13, f14) (f20, f21, f22, f23, f24) =
let t0, t1, t2, t3, t4 = fadd_zero (f10, f11, f12, f13, f14) in
let o0 = t0 -! f20 in
let o1 = t1 -! f21 in
let o2 = t2 -! f22 in
let o3 = t3 -! f23 in
let o4 = t4 -! f24 in
let out = (o0, o1, o2, o3, o4) in
FStar.Math.Lemmas.lemma_mod_plus_distr_l (as_nat5 (t0, t1, t2, t3, t4))
  (- as_nat5 (f20, f21, f22, f23, f24))
  prime;
lemma_mod_sub_distr ((as_nat5 (t0, t1, t2, t3, t4)) % prime)
  (as_nat5 (f20, f21, f22, f23, f24))
  prime;
out
Hacl.Spec.Curve25519.Field51.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Curve25519.Field51.Lemmas.fst.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Hacl.Spec.Curve25519.Field51.fst
Hacl.Spec.Curve25519.Field51.Definition.felem5 Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 FStar.Pervasives.Native.Mktuple5 Prims.nat FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.tuple5 Lib.IntTypes.uint64 Prims.unit Hacl.Spec.Curve25519.Field51.Lemmas.lemma_mod_sub_distr Prims.op_Modulus Hacl.Spec.Curve25519.Field51.Definition.as_nat5 Spec.Curve25519.prime FStar.Math.Lemmas.lemma_mod_plus_distr_l Prims.op_Minus Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.op_Subtraction_Bang Prims.l_and Prims.eq2 Spec.Curve25519.elem Hacl.Spec.Curve25519.Field51.Definition.feval Spec.Curve25519.fsub Hacl.Spec.Curve25519.Field51.fadd_zero
module Hacl.Spec.Curve25519.Field51

open Lib.Sequence
open Lib.IntTypes
open FStar.Mul
open Spec.Curve25519

open Hacl.Spec.Curve25519.Field51.Definition
open Hacl.Spec.Curve25519.Field51.Lemmas

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Seq'"

inline_for_extraction noextract
val fadd5:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> f2:felem5{felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (2, 4, 2, 2, 2) /\
      feval out == fadd (feval f1) (feval f2)}
let fadd5 (f10, f11, f12, f13, f14) (f20, f21, f22, f23, f24) =
  let o0 = f10 +! f20 in
  let o1 = f11 +! f21 in
  let o2 = f12 +! f22 in
  let o3 = f13 +! f23 in
  let o4 = f14 +! f24 in
  let out = (o0, o1, o2, o3, o4) in
  FStar.Math.Lemmas.lemma_mod_plus_distr_l
    (as_nat5 (f10, f11, f12, f13, f14)) (as_nat5 (f20, f21, f22, f23, f24)) prime;
  FStar.Math.Lemmas.lemma_mod_plus_distr_r
    ((as_nat5 (f10, f11, f12, f13, f14)) % prime) (as_nat5 (f20, f21, f22, f23, f24)) prime;
  out

inline_for_extraction noextract
val fadd_zero:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (9, 10, 9, 9, 9) /\
      feval out == feval f1}
let fadd_zero (f10, f11, f12, f13, f14) =
  let o0 = f10 +! u64 0x3fffffffffff68 in
  let o1 = f11 +! u64 0x3ffffffffffff8 in
  let o2 = f12 +! u64 0x3ffffffffffff8 in
  let o3 = f13 +! u64 0x3ffffffffffff8 in
  let o4 = f14 +! u64 0x3ffffffffffff8 in
  lemma_add_zero (f10, f11, f12, f13, f14);
  (o0, o1, o2, o3, o4)

inline_for_extraction noextract
val fsub5:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> f2:felem5{felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (9, 10, 9, 9, 9) /\
val fsub5:
    f1:felem5{felem_fits5 f1 (1, 2, 1, 1, 1)}
  -> f2:felem5{felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> out:felem5{felem_fits5 out (9, 10, 9, 9, 9) /\
    feval out == fsub (feval f1) (feval f2)}

    f1:
      Hacl.Spec.Curve25519.Field51.Definition.felem5
        {Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 f1 (1, 2, 1, 1, 1)} ->
    f2:
      Hacl.Spec.Curve25519.Field51.Definition.felem5
        {Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 f2 (1, 2, 1, 1, 1)}
  -> out:
    Hacl.Spec.Curve25519.Field51.Definition.felem5
      { Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 out (9, 10, 9, 9, 9) /\
        Hacl.Spec.Curve25519.Field51.Definition.feval out ==
        Spec.Curve25519.fsub (Hacl.Spec.Curve25519.Field51.Definition.feval f1)
          (Hacl.Spec.Curve25519.Field51.Definition.feval f2) }