( 0 is_a_unity_wrt addnat & addnat is uniquely-decomposable )