Require Import BinNat.
Extraction NoInline Ndouble Ndouble_plus_one.