Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/nat.agda @ 1376:aca9b1e67503
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Jun 2023 08:13:22 +0900 |
| parents | 8b66575d4939 |
| children | fa52d72f4bb3 |
line wrap: on
line diff
--- a/src/nat.agda Thu Jun 22 18:15:14 2023 +0900 +++ b/src/nat.agda Fri Jun 23 08:13:22 2023 +0900 @@ -248,6 +248,9 @@ refl-≤ {zero} = z≤n refl-≤ {suc x} = s≤s (refl-≤ {x}) +refl-≤≡ : {x y : ℕ } → x ≡ y → x ≤ y +refl-≤≡ refl = refl-≤ + x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)