val to_aff_point_at_infinity_lemma: unit ->
  Lemma (to_aff_point point_at_inf == aff_point_at_inf)
let to_aff_point_at_infinity_lemma () =
  let px, py = to_aff_point point_at_inf in
  assert (px == zero /% zero /\ py == one /% zero);
  assert (px == zero *% M.pow_mod #prime zero (prime - 2));
  M.lemma_pow_mod #prime zero (prime - 2);
  assert (px == zero *% (M.pow zero (prime - 2) % prime));
  M.lemma_pow_zero (prime - 2);
  assert (px == zero /\ py == zero)
val to_aff_point_at_infinity_lemma: unit ->
  Lemma (to_aff_point point_at_inf == aff_point_at_inf)
let to_aff_point_at_infinity_lemma () =
let px, py = to_aff_point point_at_inf in
assert (px == zero /% zero /\ py == one /% zero);
assert (px == zero *% M.pow_mod #prime zero (prime - 2));
M.lemma_pow_mod #prime zero (prime - 2);
assert (px == zero *% (M.pow zero (prime - 2) % prime));
M.lemma_pow_zero (prime - 2);
assert (px == zero /\ py == zero)
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
Prims.unit Spec.K256.PointOps.felem Prims._assert Prims.l_and Prims.eq2 Spec.K256.PointOps.zero Lib.NatMod.lemma_pow_zero Prims.op_Subtraction Spec.K256.PointOps.prime Spec.K256.PointOps.op_Star_Percent Prims.op_Modulus Lib.NatMod.pow Lib.NatMod.lemma_pow_mod Lib.NatMod.pow_mod Spec.K256.PointOps.op_Slash_Percent Spec.K256.PointOps.one Spec.K256.PointOps.aff_point Spec.K256.PointOps.to_aff_point Spec.K256.PointOps.point_at_inf
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()

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 to_aff_point_at_infinity_lemma: unit ->
  Lemma (to_aff_point point_at_inf == aff_point_at_inf)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.K256.PointOps.to_aff_point Spec.K256.PointOps.point_at_inf ==
      Spec.K256.PointOps.aff_point_at_inf)