# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1522288721 -32400
# Node ID 90999865d7f3e8cf7935be2bf1f513b7458c9dce
# Parent  69fc15bb4e8279c09a163fea82fed1ebac1f6dc4
some try ..

diff -r 69fc15bb4e82 -r 90999865d7f3 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Tue Mar 27 09:30:49 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Mar 29 10:58:41 2018 +0900
@@ -141,13 +141,26 @@
 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 = {!!}
+compareTri4 zero  {zero} eq _ = eq refl
+compareTri4 zero  {suc n} _ ()
+compareTri4 (suc m) {zero} _ ()
+compareTri4 (suc m) {suc n} neq with n ≟ m
+... | yes p  = λ q → neq ( cong suc p )
+... | no  p  = {!!}
 
-compareTri5 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
+compareTri4' : ∀ m {n} → n <′ m → ¬ suc n ≡ suc m
+compareTri4' zero  ()
+compareTri4' (suc n)  ≤′-refl ()
+compareTri4' (suc n)  ( ≤′-step p ) = {!!}
+
+compareTri5 : ∀ m {n} → ¬ m <′ n →  ¬ suc m <′ suc n
 compareTri5 zero    neq = {!!}
 compareTri5 (suc m) neq = {!!}
 
+compareTri5' : ∀ m {n} → m ≡   n →  ¬ suc m <′ suc n
+compareTri5' zero refl  ( ≤′-step p )  = {!!}
+compareTri5' (suc m) refl = {!!}
+
 
 compareTri :  Trichotomous  _≡_ _<′_
 compareTri zero zero = tri≈ ( λ ()) refl ( λ ())