--- a/src/ZProduct.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/ZProduct.agda	Mon May 22 19:06:25 2023 +0900
@@ -35,7 +35,7 @@
 open _==_
 
 <_,_> : (x y : HOD) → HOD
-< x , y > = (x , x ) , (x , y )
+< x , y > = (x , x) , (x , y)
 
 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
@@ -113,6 +113,11 @@
 --     lemma2 : odef (Replace' A (λ a₁ la → < a₁ , b >) ? ) (& < a , b >)
 --     lemma2 = ? -- replacement← A a A∋a ?
 
+--  & (x , x) o< next (osuc (& x))
+--  & (x , y) o< next (omax (& x) (& y))
+--  & ((x , x) , (x , y)) o< next (omax (next (osuc (& x))) (next (omax (& x) (& y))))
+--                        o≤ next (next (omax (& A) (& B)))
+
 data ZFProduct  (A B : HOD) : (p : Ordinal) → Set n where
     ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )
 
@@ -121,10 +126,10 @@
         ; odmax = omax (& A) (& B) ; <odmax = λ {y} px → lemma0 px }
    where
         lemma0 :  {A B : HOD} {x : Ordinal} → ZFProduct A B x → x o< omax (& A) (& B)
-        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b
-        ... | tri< a<b ¬b ¬c = ?
-        ... | tri≈ ¬a a=b ¬c = ?
-        ... | tri> ¬a ¬b b<a = ?
+        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b | inspect (omax a) b
+        ... | tri< a<b ¬b ¬c | record { eq = eq1 } = ?
+        ... | tri≈ ¬a a=b ¬c | record { eq = eq1 } = ?
+        ... | tri> ¬a ¬b b<a | record { eq = eq1 } = ?
 
 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ZFP A B ∋ < a , b >
 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb )