Function axiom_nonzero_from_primitive_view_eq 

pub broadcast proof fn axiom_nonzero_from_primitive_view_eq<T: ZeroablePrimitive>(n: T)

requires

!n.is_zero(),

ensures

#[trigger] nonzero_from_primitive(n)@ == n,