Commit 2019-10-24 21:13 9db43a5f
View on Github →chore(data/nat/basic): remove pos_iff_ne_zero' (#1610)
This used to be different from pos_iff_ne_zero because the latter
was phrased in terms of n > 0, not 0 < n. Since #1436 they
are the same.
chore(data/nat/basic): remove pos_iff_ne_zero' (#1610)
This used to be different from pos_iff_ne_zero because the latter
was phrased in terms of n > 0, not 0 < n. Since #1436 they
are the same.