--- a/a02/agda/practice-nat.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/agda/practice-nat.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --cubical-compatible --safe #-}
 module practice-nat where
 
 open import Data.Nat 
@@ -6,24 +7,29 @@
 open import Relation.Binary.PropositionalEquality hiding (_⇔_)
 open import logic
 
+-- data _<=_ : ℕ → ℕ → Set where
+--  z<=n : {x : ℕ} → zero <= x
+--  s<=s : {x y : ℕ} → x <= y → suc x <= suc y
+
 -- hint : it has two inputs, use recursion
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
-nat-<> = {!!}  
+nat-<>   (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 
 -- hint : use recursion
 nat-<≡ : { x : ℕ } → x < x → ⊥
-nat-<≡ = {!!}
+nat-<≡ (s≤s x<x) = nat-<≡ x<x
 
 -- hint : use refl and recursion
 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
-nat-≡< = {!!}
+nat-≡< refl (s≤s x<y) = nat-≡< refl x<y
 
 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
-¬a≤a = {!!}
+¬a≤a (s≤s lt) = ¬a≤a lt
 
 -- hint : make case with la first
-a<sa : {la : ℕ} → la < suc la 
-a<sa = {!!}
+a<sa : {i : ℕ} → i < suc i 
+a<sa {zero} = s≤s z≤n
+a<sa {suc i} =  s≤s a<sa 
 
 -- hint  : ¬ has an input, use recursion
 =→¬< : {x : ℕ  } → ¬ ( x < x )