# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1522375746 -32400
# Node ID 8634f448e69963f2e40a9683813764c223d2822a
# Parent  9df8103bc49333e6250be31ea5564bbf416c3706
minor fix

diff -r 9df8103bc493 -r 8634f448e699 redBlackTreeTest.agda
--- 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)