--- a/src/nat.agda	Wed Jun 14 12:34:45 2023 +0900
+++ b/src/nat.agda	Fri Jun 16 08:49:25 2023 +0900
@@ -252,6 +252,12 @@
 px≤py {zero} {suc y} lt = z≤n
 px≤py {suc x} {suc y} (s≤s lt) = lt 
 
+sx≤py→x≤y : {x y : ℕ } → suc x ≤ suc y → x  ≤ y 
+sx≤py→x≤y (s≤s lt) = lt
+
+sx<py→x<y : {x y : ℕ } → suc x < suc y → x  < y 
+sx<py→x<y (s≤s lt) = lt
+
 sx≤y→x≤y : {x y : ℕ } → suc x ≤ y → x  ≤ y 
 sx≤y→x≤y {zero} {suc y} (s≤s le) = z≤n
 sx≤y→x≤y {suc x} {suc y} (s≤s le) = s≤s (sx≤y→x≤y {x} {y} le)
@@ -724,3 +730,4 @@
             ; ind = λ {p} prev → ind p prev
           } 
 
+