val abs (a b: nat) : nat
let abs (a:nat) (b:nat) : nat =
  if a < b then b - a else a - b
val abs (a b: nat) : nat
let abs (a b: nat) : nat =
if a < b then b - a else 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 Prims.op_Subtraction Prims.bool
module Hacl.Spec.Karatsuba.Lemmas

open FStar.Mul
open Lib.IntTypes

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

type sign =
  | Positive
  | Negative
val abs (a b: nat) : nat
a: Prims.nat -> b: Prims.nat -> Prims.nat