--- a/redBlackTreeTest.agda	Thu Mar 29 20:23:51 2018 +0900
+++ b/redBlackTreeTest.agda	Fri Mar 30 10:17:07 2018 +0900
@@ -148,14 +148,19 @@
 ... | no p = no {!!}
 
 compareTri20 : {n : ℕ} -> ¬ suc n ≤′ zero
-compareTri20 {zero} = {!!}
-compareTri20 {suc n} = {!!}
+compareTri20 () 
+
 
 compareTri21 : (n m : ℕ) -> suc n ≤′ suc m ->  n ≤′ m
 compareTri21 _ _  ≤′-refl = ≤′-refl
+compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
+  where
+        compareTri23 : (n : ℕ) -> suc n ≤′ suc zero -> suc n ≤′ zero ->  n ≤′ zero
+        compareTri23 zero ( ≤′-step p ) _ =   ≤′-refl
+        compareTri23 zero ≤′-refl _ =   ≤′-refl
+        compareTri23 (suc n1) ( ≤′-step p ) ()
 compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
 compareTri21 zero zero ( ≤′-step p ) = ≤′-refl
-compareTri21 (suc n1) zero = {!!}
    
 
 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)