mathlib3

refactor(*): assume `≠0` instead of `0 < _`

#17612

Open