Commit 2025-12-05 15:16 c882ca73

chore: make sure that Nat.AtLeastTwo instances are constructive (#32467) @riccardobrasca noticed a few weeks ago that you cannot write the symbol 2 in an abstract ring R without relying on the axiom of choice. After investigating a bit, we realized that this boiled down to the use of excluded midde (through lia) in Nat.instAtLeastTwoHAddOfNat. While I am by no means advocating for widespread support of constructive users in Mathlib, I think this one is ridiculous enough that it needs fixing (and the fix is really easy).