val bn_add1_lemma:
    #t:limb_t
  -> #aLen:size_pos
  -> a:lbignum t aLen
  -> b1:limb t ->
  Lemma (let (c, res) = bn_add1 a b1 in
    v c * pow2 (bits t * aLen) + bn_v res == bn_v a + v b1)
let bn_add1_lemma #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_add1_lemma a b1
val bn_add1_lemma:
    #t:limb_t
  -> #aLen:size_pos
  -> a:lbignum t aLen
  -> b1:limb t ->
  Lemma (let (c, res) = bn_add1 a b1 in
    v c * pow2 (bits t * aLen) + bn_v res == bn_v a + v b1)
let bn_add1_lemma #t #aLen a b1 =
Hacl.Spec.Bignum.Addition.bn_add1_lemma a b1
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_pos Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Definitions.limb Hacl.Spec.Bignum.Addition.bn_add1_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
val bn_add1_lemma:
    #t:limb_t
  -> #aLen:size_pos
  -> a:lbignum t aLen
  -> b1:limb t ->
  Lemma (let (c, res) = bn_add1 a b1 in
    v c * pow2 (bits t * aLen) + bn_v res == bn_v a + v b1)
a: Hacl.Spec.Bignum.Definitions.lbignum t aLen -> b1: Hacl.Spec.Bignum.Definitions.limb t
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = Hacl.Spec.Bignum.bn_add1 a b1 in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ c res = _ in
          Lib.IntTypes.v c * Prims.pow2 (Lib.IntTypes.bits t * aLen) +
          Hacl.Spec.Bignum.Definitions.bn_v res ==
          Hacl.Spec.Bignum.Definitions.bn_v a + Lib.IntTypes.v b1)
        <:
        Type0))