Theorem GCongr.natCast_lt_natCast

Modification history

2025-10-27 16:35
Mathlib/Data/Nat/Cast/Order/Basic.lean
feat(gcongr): support `@[gcongr]` for `Monotone` and friends (#28339) …
Deleted GCongr.natCast_lt_natCastView on Github →
2024-08-16 22:15
Mathlib/Data/Nat/Cast/Order/Basic.lean
chore: Let `gcongr` know about `Nat.cast_lt` (#15879) …
Added GCongr.natCast_lt_natCastView on Github →