val sign_abs: a:nat -> b:nat ->
  Pure (tuple2 sign nat)
  (requires True)
  (ensures  fun (s, res) -> res == abs a b /\
    s == (if a < b then Negative else Positive))
let sign_abs a b =
  if a < b then (Negative, b - a) else (Positive, a - b)
val sign_abs: a:nat -> b:nat ->
  Pure (tuple2 sign nat)
  (requires True)
  (ensures  fun (s, res) -> res == abs a b /\
    s == (if a < b then Negative else Positive))
let sign_abs a b =
if a < b then (Negative, b - a) else (Positive, a - b)
Hacl.Spec.Karatsuba.Lemmas.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.Karatsuba.Lemmas.fst
Prims.nat Prims.op_LessThan FStar.Pervasives.Native.Mktuple2 Hacl.Spec.Karatsuba.Lemmas.sign Hacl.Spec.Karatsuba.Lemmas.Negative Prims.op_Subtraction Prims.bool Hacl.Spec.Karatsuba.Lemmas.Positive FStar.Pervasives.Native.tuple2
module Hacl.Spec.Karatsuba.Lemmas

open FStar.Mul
open Lib.IntTypes

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

type sign =
  | Positive
  | Negative

let abs (a:nat) (b:nat) : nat =
  if a < b then b - a else a - b

val sign_abs: a:nat -> b:nat ->
  Pure (tuple2 sign nat)
  (requires True)
  (ensures  fun (s, res) -> res == abs a b /\
    s == (if a < b then Negative else Positive))
val sign_abs: a:nat -> b:nat ->
  Pure (tuple2 sign nat)
  (requires True)
  (ensures  fun (s, res) -> res == abs a b /\
    s == (if a < b then Negative else Positive))
a: Prims.nat -> b: Prims.nat -> Prims.Pure (Hacl.Spec.Karatsuba.Lemmas.sign * Prims.nat)