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_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;
FStar.Math.Lemmas.lemma_mod_plus (a - (b % n)) (- (b / n)) n
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.int Prims.pos FStar.Math.Lemmas.lemma_mod_plus Prims.op_Subtraction Prims.op_Modulus Prims.op_Minus Prims.op_Division Prims.unit FStar.Math.Lemmas.distributivity_sub_left FStar.Math.Lemmas.lemma_div_mod
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)
val lemma_mod_sub_distr: a:int -> b:int -> n:pos ->
  Lemma ((a - b % n) % n = (a - b) % n)
a: Prims.int -> b: Prims.int -> n: Prims.pos
  -> FStar.Pervasives.Lemma (ensures (a - b % n) % n = (a - b) % n)