RFC: drop `Nat.AtLeastTwo`

Status quo

In Lean 4, numerical literals (e.g., (3 : α)) are in fact expressions of the form OfNat.ofNat 3 and depend on a typeclass instance

instance : OfNat α n

available for this particular type & numerical literal.

In Mathlib, there are a few commonly used OfNat instances:

• [One M] : OfNat M 1;
• [Zero M] : OfNat M 0;
• [NatCast R] {n} [n.AtLeastTwo] : OfNat R n.

There are also instances like [NeZero n] : OfNat PNat n, which are probably out of the scope of this discussion.

Why Nat.AtLeastTwo?

If we just drop [n.AtLeastTwo] in the [NatCast R] : OfNat R n instance, then for a ring R, we'll have 2 different instances for [OfNat R 0] and [OfNat R 1]. While we can ensure definitional equality for each specific type, this won't work for a generic ring.

Why change?

Leo is working on grind and Groebner bases, and he uses [∀ n, OfNat α n] everywhere. If we want his code to work for Mathlib type, then we need to ensure [∀ n, OfNat α n] for our types or negotiate another approach.

Proposal 1

Drop [Nat.AtLeastTwo] and simplify one ofNat _ 0 to another.

Downside: it's easy to arrive at a situation when a lemma seems to apply but it doesn't, because it uses a wrong zero or one. This manifest as 1 = 1 not being solved by rfl. While we can ensure defeq for each concrete type (e.g., Real, by removing irreducible_def), we can't make it work for {M : Type*} [AddMonoidWithOne M] without rewriting the definition of AddMonoidWithOne (or modifying some other part of the system).

Proposal 2

Drop [Nat.AtLeastTwo _] and rewrite AddMonoidWithOne so that it no longer extends Zero (via AddMonoid) or One, and repeats the AddMonoid axioms using zero and one coming from ∀ n, OfNat M n.

We should write a linter that verifies that no instance of AddMonoidWithOne (or another class down the road) conflicts with Zero/One instance coming from other source.