Commit 2026-10-31 01:50 156eea30

View on Github →

chore(Data/Nat/Cast): remove redundant order instances (#45515) Remove three redundant instance assumptions:

  • [AddRightMono α] from Nat.one_sub_one_div_cast_nonneg;
  • [AddLeftMono α] from Nat.one_sub_one_div_cast_le_one;
  • [IsOrderedRing α] from Nat.cast_tsub. The remaining ordered-algebra assumptions supply these instances. All three proofs are unchanged.

Estimated changes

modified theorem Nat.cast_tsub