val bn_sub_lemma:
    #t:limb_t
  -> #aLen:size_nat
  -> #bLen:size_nat{bLen <= aLen}
  -> a:lbignum t aLen
  -> b:lbignum t bLen ->
  Lemma (let (c_out, res) = bn_sub a b in
    bn_v res - v c_out * pow2 (bits t * aLen) == bn_v a - bn_v b)
let bn_sub_lemma #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_sub_lemma a b
val bn_sub_lemma:
    #t:limb_t
  -> #aLen:size_nat
  -> #bLen:size_nat{bLen <= aLen}
  -> a:lbignum t aLen
  -> b:lbignum t bLen ->
  Lemma (let (c_out, res) = bn_sub a b in
    bn_v res - v c_out * pow2 (bits t * aLen) == bn_v a - bn_v b)
let bn_sub_lemma #t #aLen #bLen a b =
Hacl.Spec.Bignum.Addition.bn_sub_lemma a b
Hacl.Spec.Bignum.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Squaring.fst.checked Hacl.Spec.Bignum.Multiplication.fst.checked Hacl.Spec.Bignum.Lib.fst.checked Hacl.Spec.Bignum.Karatsuba.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Spec.Bignum.Comparison.fst.checked Hacl.Spec.Bignum.Addition.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Hacl.Spec.Bignum.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThanOrEqual Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Addition.bn_sub_lemma Prims.unit
module Hacl.Spec.Bignum

module Loops = Lib.LoopCombinators


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

let bn_add1 #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_add1 a b1

let bn_add1_lemma #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_add1_lemma a b1

let bn_sub1 #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_sub1 a b1

let bn_sub1_lemma #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_sub1_lemma a b1

let bn_add #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_add a b

let bn_add_lemma #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_add_lemma a b

let bn_sub #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_sub a b
val bn_sub_lemma:
    #t:limb_t
  -> #aLen:size_nat
  -> #bLen:size_nat{bLen <= aLen}
  -> a:lbignum t aLen
  -> b:lbignum t bLen ->
  Lemma (let (c_out, res) = bn_sub a b in
    bn_v res - v c_out * pow2 (bits t * aLen) == bn_v a - bn_v b)
a: Hacl.Spec.Bignum.Definitions.lbignum t aLen -> b: Hacl.Spec.Bignum.Definitions.lbignum t bLen
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = Hacl.Spec.Bignum.bn_sub a b in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ c_out res = _ in
          Hacl.Spec.Bignum.Definitions.bn_v res -
          Lib.IntTypes.v c_out * Prims.pow2 (Lib.IntTypes.bits t * aLen) ==
          Hacl.Spec.Bignum.Definitions.bn_v a - Hacl.Spec.Bignum.Definitions.bn_v b)
        <:
        Type0))