[ cleanup ] Make Nat's NonZero to be an alias for IsSucc

[buzden]

Description

Historically for some strange reason in Data.Nat we have two equivalent definitions: IsSucc and NonZero. Other standard types have standard pattern of Is<Constructor> type, ItIs<Constructor> constructor of proof and isIt<Constructor> for Dec Is<Consturctor>. IsSucc follows this pattern, when NonZero does not. However, NonZero is a handy name for this.

But the fact that there are two different types for this and the fact that some standard and non-standard functions use one of them, and others use the other, triggers a lot of people (I personally know around five of them).

What I suggest is to make NonZero to be an alias for IsSucc and to declare a deprecated alias for original constructor of NonZero to be backward compatible at least on usages at RHS.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[andrevidela]

If we can fix frex, this looks good to me

[buzden]

If we can fix frex, this looks good to me

Right, this seems to be not much a strech for frex, I made a PR there

[mattpolzin]

Looks good to me too. Seems like we can get this merged whenever.