val sub_carry (x y: nat64) (c: bit) : nat64 & bit
let sub_carry (x y:nat64) (c:bit) : nat64 & bit
  =
  if x - (y + c) < 0 then
    (x - (y + c) + pow2_64, 1)
  else
    (x - (y + c)), 0
val sub_carry (x y: nat64) (c: bit) : nat64 & bit
let sub_carry (x y: nat64) (c: bit) : nat64 & bit =
if x - (y + c) < 0 then (x - (y + c) + pow2_64, 1) else (x - (y + c)), 0
Vale.Curve25519.FastUtil_helpers.fsti.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_defs.fst.checked prims.fst.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Curve25519.FastUtil_helpers.fsti
Vale.Def.Types_s.nat64 Vale.Curve25519.Fast_defs.bit Prims.op_LessThan Prims.op_Subtraction Prims.op_Addition FStar.Pervasives.Native.Mktuple2 Vale.Def.Words_s.pow2_64 Prims.bool FStar.Pervasives.Native.tuple2
module Vale.Curve25519.FastUtil_helpers

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open FStar.Tactics
open FStar.Tactics.CanonCommSemiring
open Vale.Curve25519.Fast_defs

let int_canon = fun _ -> norm [delta; zeta; iota]; int_semiring () //; dump "Final"

let sub_carry (x y:nat64) (c:bit) : nat64 & bit
val sub_carry (x y: nat64) (c: bit) : nat64 & bit
x: Vale.Def.Types_s.nat64 -> y: Vale.Def.Types_s.nat64 -> c: Vale.Curve25519.Fast_defs.bit
  -> Vale.Def.Types_s.nat64 * Vale.Curve25519.Fast_defs.bit