val lemma_proj_aff_id (p:aff_point) :
  Lemma (to_aff_point (to_proj_point p) == p)
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)
val lemma_proj_aff_id (p:aff_point) :
  Lemma (to_aff_point (to_proj_point p) == p)
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)
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.l_and Prims.b2t Prims.op_Equality Prims.unit Lib.NatMod.lemma_div_mod_prime_one Spec.K256.PointOps.prime Spec.K256.PointOps.op_Slash_Percent Spec.K256.PointOps.to_aff_point FStar.Pervasives.Native.Mktuple3 Spec.K256.PointOps.one Spec.K256.PointOps.proj_point Spec.K256.PointOps.to_proj_point
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
val lemma_proj_aff_id (p:aff_point) :
  Lemma (to_aff_point (to_proj_point p) == p)
p: Spec.K256.PointOps.aff_point
  -> FStar.Pervasives.Lemma
    (ensures Spec.K256.PointOps.to_aff_point (Spec.K256.PointOps.to_proj_point p) == p)