# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1522316320 -32400
# Node ID 8595a7ffba8bbd5d23a4e9db442be3324033cc8a
# Parent  90999865d7f3e8cf7935be2bf1f513b7458c9dce
fix

diff -r 90999865d7f3 -r 8595a7ffba8b redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Thu Mar 29 10:58:41 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Mar 29 18:38:40 2018 +0900
@@ -141,26 +141,25 @@
 compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
 
 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
-compareTri4 zero  {zero} eq _ = eq refl
-compareTri4 zero  {suc n} _ ()
-compareTri4 (suc m) {zero} _ ()
-compareTri4 (suc m) {suc n} neq with n ≟ m
-... | yes p  = λ q → neq ( cong suc p )
-... | no  p  = {!!}
+compareTri4 m {n} with n ≟ m
+... | yes refl  = λ x y → x refl
+... | no  p  = λ x y → p ( cong pred y )
 
-compareTri4' : ∀ m {n} → n <′ m → ¬ suc n ≡ suc m
-compareTri4' zero  ()
-compareTri4' (suc n)  ≤′-refl ()
-compareTri4' (suc n)  ( ≤′-step p ) = {!!}
+<′dec : Set
+<′dec = ∀ m n → Dec ( m ≤′ n )
+ 
+is≤′ :  <′dec
+is≤′  zero zero = yes ≤′-refl
+is≤′  zero (suc n) = yes {!!}
+is≤′  (suc m) (zero) = no ( \ () )
+is≤′  (suc m) (suc n) with is≤′ m n
+... | yes p = yes {!!}
+... | no p = no {!!}
 
 compareTri5 : ∀ m {n} → ¬ m <′ n →  ¬ suc m <′ suc n
-compareTri5 zero    neq = {!!}
-compareTri5 (suc m) neq = {!!}
-
-compareTri5' : ∀ m {n} → m ≡   n →  ¬ suc m <′ suc n
-compareTri5' zero refl  ( ≤′-step p )  = {!!}
-compareTri5' (suc m) refl = {!!}
-
+compareTri5  m {n} with (is≤′ m n)
+... | yes p = {!!}
+... | no p = {!!}
 
 compareTri :  Trichotomous  _≡_ _<′_
 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())