Theorem Nat.one_le_of_lt

Modification history

2024-04-05 18:00

Mathlib/Data/Nat/Defs.lean

chore: reduce mathlib dependencies in Data.Nat.Defs (#11918) …

Modified Nat.one_le_of_lt View on Github →

2024-03-26 23:09

Mathlib/Data/Nat/Defs.lean

chore(Data/Nat): Use Std lemmas (#11661) …

Modified Nat.one_le_of_lt View on Github →

2022-12-10 13:28

Mathlib/Data/Nat/Order/Basic.lean

feat: port Data.Nat.Order.Basic (#907) …

Added Nat.one_le_of_lt View on Github →