--- a/redBlackTreeTest.agda	Mon Mar 26 23:44:02 2018 +0900
+++ b/redBlackTreeTest.agda	Tue Mar 27 09:30:49 2018 +0900
@@ -132,22 +132,35 @@
 compareTri1 zero =   ≤′-refl 
 compareTri1 (suc n) =  ≤′-step ( compareTri1 n )
 
-compareTri2 : (n m : ℕ) -> (suc n) ≤′ m -> suc (suc n) ≤′ suc m
+compareTri2 : (n m : ℕ) -> n ≤′ m -> suc n ≤′ suc m
 compareTri2 _ _  ≤′-refl = ≤′-refl 
-compareTri2 n (suc m) ( ≤′-step p ) =  ≤′-step { suc (suc n) }  ( compareTri2 n m p )
+compareTri2 n (suc m) ( ≤′-step p ) =  ≤′-step { suc n }  ( compareTri2 n m p )
+
+compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
+compareTri3 zero    ()
+compareTri3 (suc m) eq = compareTri3 m (cong pred eq)
+
+compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
+compareTri4 zero    neq = {!!}
+compareTri4 (suc m) neq = {!!}
+
+compareTri5 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
+compareTri5 zero    neq = {!!}
+compareTri5 (suc m) neq = {!!}
+
 
 compareTri :  Trichotomous  _≡_ _<′_
 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
 compareTri zero (suc n) = tri< ( compareTri1 n )  ( λ ()) ( λ ())
 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
 compareTri (suc n) (suc m) with compareTri n m
-... | tri≈ p refl r = tri≈ {!!} refl {!!}
-... | tri< p q r = tri<  (compareTri2 n m p ) {!!} {!!}
-... | tri> p q r = tri> {!!} {!!}  (compareTri2 m n r )
+... | tri< p q r = tri<  (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
+... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
+... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )
 
 compareDecTest : (n n1 : Node ℕ ℕ) -> ( key n ≡ key n1 ) ∨ ( ¬  key n ≡ key n1 )
 compareDecTest n n1 with (key n) ≟ (key n1)
-...  | yes p = pi1 p
+...  | yes p  = pi1  p
 ...  | no ¬p  = pi2 ¬p