val aff_point_negate_lemma (p:aff_point) :
  Lemma (aff_point_add (aff_point_negate p) p == aff_point_at_inf)
let aff_point_negate_lemma p =
  let p_neg = aff_point_negate p in
  let px, py = p in
  let qx, qy = p_neg in
  assert (qx = px /\ qy = (-py) % prime);
  assert (aff_point_add p_neg p == aff_point_at_inf)
val aff_point_negate_lemma (p:aff_point) :
  Lemma (aff_point_add (aff_point_negate p) p == aff_point_at_inf)
let aff_point_negate_lemma p =
let p_neg = aff_point_negate p in
let px, py = p in
let qx, qy = p_neg in
assert (qx = px /\ qy = (- py) % prime);
assert (aff_point_add p_neg p == aff_point_at_inf)
Spec.K256.Lemmas.fst.checked
Spec.K256.PointOps.fst.checked prims.fst.checked Lib.NatMod.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Math.Euclid.fsti.checked FStar.Calc.fsti.checked
Spec.K256.Lemmas.fst
Spec.K256.PointOps.aff_point Spec.K256.PointOps.felem Prims._assert Prims.eq2 Spec.K256.PointOps.aff_point_add Spec.K256.PointOps.aff_point_at_inf Prims.unit Prims.l_and Prims.b2t Prims.op_Equality Prims.int Prims.op_Modulus Prims.op_Minus Spec.K256.PointOps.prime Spec.K256.PointOps.aff_point_negate
module Spec.K256.Lemmas

open FStar.Mul

open Spec.K256.PointOps

module Euclid = FStar.Math.Euclid
module M = Lib.NatMod

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

assume val prime_lemma: unit -> Lemma (Euclid.is_prime prime)

let lemma_aff_is_point_at_inf p =
  prime_lemma ();
  let (px, py, pz) = p in
  M.lemma_div_mod_prime_is_zero #prime px pz;
  M.lemma_div_mod_prime_is_zero #prime py pz


let lemma_proj_aff_id p =
  let (px, py) = p in
  let (pX, pY, pZ) = to_proj_point p in
  assert (pX = px /\ pY = pY /\ pZ = one);
  let (rx, ry) = to_aff_point (pX, pY, pZ) in
  assert (rx = (pX /% pZ) /\ ry = (pY /% pZ));
  M.lemma_div_mod_prime_one #prime pX;
  M.lemma_div_mod_prime_one #prime pY;
  assert (rx = pX /\ ry = pY)

let aff_point_at_inf_lemma p = ()

let aff_point_add_assoc_lemma p q s = admit()

let aff_point_add_comm_lemma p q = admit()
val aff_point_negate_lemma (p:aff_point) :
  Lemma (aff_point_add (aff_point_negate p) p == aff_point_at_inf)
p: Spec.K256.PointOps.aff_point
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.K256.PointOps.aff_point_add (Spec.K256.PointOps.aff_point_negate p) p ==
      Spec.K256.PointOps.aff_point_at_inf)