Function nonzero_spec_get 

pub open spec fn nonzero_spec_get<T: ZeroablePrimitive>(n: NonZero<T>) -> T

{ n@ }