let add_and_double1_0 a b nqp1 =
  let x_3, z_3 = nqp1 in
  let c = x_3 +% z_3 in
  let d = x_3 -% z_3 in

  let da = d *% a in
  let cb = c *% b in
  let x_3 = da +% cb in
  let z_3 = da -% cb in
  (x_3, z_3)
let add_and_double1_0 a b nqp1 =
let x_3, z_3 = nqp1 in
let c = x_3 +% z_3 in
let d = x_3 -% z_3 in
let da = d *% a in
let cb = c *% b in
let x_3 = da +% cb in
let z_3 = da -% cb in
(x_3, z_3)
Hacl.Spec.Curve25519.AddAndDouble.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Curve25519.AddAndDouble.fst
Spec.Curve25519.elem FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 Spec.Curve25519.op_Subtraction_Percent Spec.Curve25519.op_Plus_Percent Spec.Curve25519.op_Star_Percent
module Hacl.Spec.Curve25519.AddAndDouble

open FStar.Mul
open Lib.IntTypes
open Spec.Curve25519
val add_and_double1_0 : a: Spec.Curve25519.elem ->
    b: Spec.Curve25519.elem ->
    nqp1: (Spec.Curve25519.elem * Spec.Curve25519.elem)
  -> Spec.Curve25519.elem * Spec.Curve25519.elem

    a: Spec.Curve25519.elem ->
    b: Spec.Curve25519.elem ->
    nqp1: (Spec.Curve25519.elem * Spec.Curve25519.elem)
  -> Spec.Curve25519.elem * Spec.Curve25519.elem