--- a/redBlackTreeTest.agda	Fri Mar 30 10:52:51 2018 +0900
+++ b/redBlackTreeTest.agda	Fri Mar 30 11:09:06 2018 +0900
@@ -176,11 +176,14 @@
 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
+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 )
 
+compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
+compareTri4 m = contraposition ( λ x → cong pred x )
+
 -- compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
 compareTri6  m {n} = λ x y → x (compareTri21 _ _ y)