val lemma_prime: unit ->
  Lemma (pow2 255 % prime = 19)
let lemma_prime () =
  assert_norm (pow2 255 % prime = 19 % prime);
  assert_norm (19 < prime);
  FStar.Math.Lemmas.modulo_lemma 19 prime
val lemma_prime: unit ->
  Lemma (pow2 255 % prime = 19)
let lemma_prime () =
assert_norm (pow2 255 % prime = 19 % prime);
assert_norm (19 < prime);
FStar.Math.Lemmas.modulo_lemma 19 prime
Hacl.Spec.Curve25519.Field51.Lemmas.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Impl.Curve25519.Lemmas.fst.checked FStar.UInt32.fsti.checked FStar.Tactics.Canon.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Hacl.Spec.Curve25519.Field51.Lemmas.fst
Prims.unit FStar.Math.Lemmas.modulo_lemma Spec.Curve25519.prime FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.op_Equality Prims.int Prims.op_Modulus Prims.pow2
module Hacl.Spec.Curve25519.Field51.Lemmas

open FStar.Mul
open Lib.Sequence
open Lib.IntTypes

open FStar.Tactics
open FStar.Tactics.Canon

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

module BSeq = Lib.ByteSequence
module LSeq = Lib.Sequence

#reset-options "--z3rlimit 50 --using_facts_from '* -FStar.Seq -FStar.Tactics'"

val lemma_mod_sub_distr: a:int -> b:int -> n:pos ->
  Lemma ((a - b % n) % n = (a - b) % n)
let lemma_mod_sub_distr a b n =
  FStar.Math.Lemmas.lemma_div_mod b n;
  FStar.Math.Lemmas.distributivity_sub_left 0 (b / n) n;
  // (a - b) % n == (a - (b % n) - (b / n) * n) % n
  FStar.Math.Lemmas.lemma_mod_plus (a - (b % n)) (-(b / n)) n

val lemma_mul5_distr_r:
  a:nat -> b:nat -> c:nat -> d:nat -> e:nat -> f:nat ->
  Lemma ((a + b + c + d + e) * f == a * f + b * f + c * f + d * f + e * f)
let lemma_mul5_distr_r a b c d e f = ()

val lemma_mul5_distr_l:
  a:nat -> b:nat -> c:nat -> d:nat -> e:nat -> f:nat ->
  Lemma (a * (b + c + d + e + f) == a * b + a * c + a * d + a * e + a * f)
let lemma_mul5_distr_l a b c d e f = ()

val lemma_mul_assos_3:
  a:nat -> b:nat -> c:nat ->
  Lemma (a * b * c == a * (b * c))
let lemma_mul_assos_3 a b c = ()

val lemma_mul_assos_4:
  a:nat -> b:nat -> c:nat -> d:nat ->
  Lemma (a * b * c * d == a * (b * c * d))
let lemma_mul_assos_4 a b c d = ()

val lemma_mul_assos_5:
  a:nat -> b:nat -> c:nat -> d:nat -> e:nat ->
  Lemma (a * b * c * d * e == a * (b * c * d * e))
let lemma_mul_assos_5 a b c d e = ()

val lemma_mul_assos_6:
  a:nat -> b:nat -> c:nat -> d:nat -> e:nat -> f:nat ->
  Lemma (a * b * c * d * e * f == a * (b * c * d * e * f))
let lemma_mul_assos_6 a b c d e f = ()

val lemma_add_le:a:nat -> b:nat -> c:nat -> d:nat ->
  Lemma
  (requires a <= b /\ c <= d)
  (ensures  a + c <= b + d)
let lemma_add_le a b c d = ()

val lemma_mul_le:a:nat -> b:nat -> c:nat -> d:nat ->
  Lemma
  (requires a <= b /\ c <= d)
  (ensures  a * c <= b * d)
let lemma_mul_le a b c d = ()

val lemma_prime: unit ->
  Lemma (pow2 255 % prime = 19)
val lemma_prime: unit ->
  Lemma (pow2 255 % prime = 19)
_: Prims.unit -> FStar.Pervasives.Lemma (ensures Prims.pow2 255 % Spec.Curve25519.prime = 19)