val lemma_aff_is_point_at_inf: p:proj_point ->
  Lemma (let px, py, pz = p in
    is_aff_point_at_inf (to_aff_point p) == (pz = 0 || (px = 0 && py = 0)))
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_aff_is_point_at_inf: p:proj_point ->
  Lemma (let px, py, pz = p in
    is_aff_point_at_inf (to_aff_point p) == (pz = 0 || (px = 0 && py = 0)))
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
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.proj_point Spec.K256.PointOps.felem Lib.NatMod.lemma_div_mod_prime_is_zero Spec.K256.PointOps.prime Prims.unit Spec.K256.Lemmas.prime_lemma
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)
val lemma_aff_is_point_at_inf: p:proj_point ->
  Lemma (let px, py, pz = p in
    is_aff_point_at_inf (to_aff_point p) == (pz = 0 || (px = 0 && py = 0)))
p: Spec.K256.PointOps.proj_point
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = p in
        (let FStar.Pervasives.Native.Mktuple3 #_ #_ #_ px py pz = _ in
          Spec.K256.PointOps.is_aff_point_at_inf (Spec.K256.PointOps.to_aff_point p) ==
          (pz = 0 || px = 0 && py = 0))
        <:
        Type0))