Add ≤‴-irrelevant
to Data.Nat.Properties
#2503
Merged
Loading
≤‴-irrelevant
to Data.Nat.Properties
#2503