--- a/redBlackTreeTest.agda	Thu Mar 29 18:38:40 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Mar 29 19:38:49 2018 +0900
@@ -136,15 +136,6 @@
 compareTri2 _ _  ≤′-refl = ≤′-refl 
 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 m {n} with n ≟ m
-... | yes refl  = λ x y → x refl
-... | no  p  = λ x y → p ( cong pred y )
-
 <′dec : Set
 <′dec = ∀ m n → Dec ( m ≤′ n )
  
@@ -156,11 +147,35 @@
 ... | yes p = yes {!!}
 ... | no p = no {!!}
 
+compareTri20 : {n : ℕ} -> ¬ suc n ≤′ zero
+compareTri20 {zero} = {!!}
+compareTri20 {suc n} = {!!}
+
+compareTri21 : (n m : ℕ) -> suc n ≤′ suc m ->  n ≤′ m
+compareTri21 _ _  ≤′-refl = ≤′-refl
+compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
+compareTri21 zero zero _ = ≤′-refl
+compareTri21 (suc zero) zero _ = {!!}
+compareTri21 (suc (suc n)) zero _ = {!!}
+
+
+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 m {n} with n ≟ m
+... | yes refl  = λ x y → x refl
+... | no  p  = λ x y → p ( cong pred y )
+
 compareTri5 : ∀ m {n} → ¬ m <′ n →  ¬ suc m <′ suc n
 compareTri5  m {n} with (is≤′ m n)
 ... | yes p = {!!}
 ... | no p = {!!}
 
+compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
+compareTri6  m {n} = λ x y → x (compareTri21 _ _ y)
+
 compareTri :  Trichotomous  _≡_ _<′_
 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
 compareTri zero (suc n) = tri< ( compareTri1 n )  ( λ ()) ( λ ())