Commit 2025-08-22 06:26 1964d7e7
View on Github →refactor: syntactically generalise the Nontrivial (Fin n) instance (#28638)
This way, it applies to expression not of the form _ + 1.
Also move Nat.AtLeastTwo earlier to satisfy the assert_not_exists in Data.Fin.Basic.
From ForbiddenMatrix