# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1679398136 -32400
# Node ID 0d278b809c010fe6a53803d6fbb15093e52a0a1f
# Parent  a27f28dbed879e71245ee3b4ecd090d5835417d0
...

diff -r a27f28dbed87 -r 0d278b809c01 src/generic-filter.agda
--- a/src/generic-filter.agda	Tue Mar 21 11:19:15 2023 +0900
+++ b/src/generic-filter.agda	Tue Mar 21 20:28:56 2023 +0900
@@ -374,6 +374,17 @@
 TCS : (G : HOD) → Set (Level.suc n)
 TCS G = {x y : HOD} → G ∋ x → x ∋ y → G ∋ y
 
+lemma233 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
+      → (C : CountableModel )
+      → ctl-M C ∋ L → {x : HOD } → ( ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C ))) ∋ x
+      → ctl-M C ∋  val x ( ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C )))
+lemma233 P L p0 LPP Lp0 C ML {x} Gx = subst (λ k → odef M (& (val k _))) *iso (lm00 (& x) ? ) where
+    M = ctl-M C
+    pind : (x : Ordinal) → ((y : Ordinal) → y o< x → ? → M ∋ val (* y) (PDHOD L p0 C)) → ? → M ∋ val (* x) (PDHOD L p0 C)
+    pind x prev = ?
+    lm00 : (x : Ordinal) → PDHOD L p0 C ∋ * x → M ∋ val (* x) (PDHOD L p0 C)
+    lm00  x gx = TransFinite0 {λ x →  PDHOD L p0 C ∋ * x →  M ∋ val (* x) (PDHOD L p0 C)} pind x gx
+
 val∋→∋p :  {G : HOD} → (TCS G) → {x y : HOD} → {p : HOD} → G ∋ p  → ( val x G ∋ val y G ) → x ∋ < y , p >
 val∋→∋p = ?
 
diff -r a27f28dbed87 -r 0d278b809c01 src/nat.agda
--- a/src/nat.agda	Tue Mar 21 11:19:15 2023 +0900
+++ b/src/nat.agda	Tue Mar 21 20:28:56 2023 +0900
@@ -280,9 +280,16 @@
 minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y)  ≡ x - z
 minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z  ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z})
 
++cancel<l : (x z : ℕ ) {y : ℕ} → y + x < y + z → x < z
++cancel<l x z {zero} lt = lt
++cancel<l x z {suc y} (s≤s lt) = +cancel<l x z {y} lt
+
++cancel<r : (x z : ℕ ) {y : ℕ} → x + y < z + y → x < z
++cancel<r x z {y} lt = +cancel<l x z (subst₂ (λ j k → j < k ) (+-comm x _) (+-comm z _) lt ) 
+
 y-x<y : {x y : ℕ } → 0 < x → 0 < y  → y - x  <  y
 y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y)
-... | tri< a ¬b ¬c = +-cancelʳ-<  (y - x) _ ( begin
+... | tri< a ¬b ¬c = +cancel<r (y - x) _ ( begin
          suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩
          suc y  ≡⟨ +-comm 1 _ ⟩
          y + suc 0  ≤⟨ +-mono-≤ ≤-refl 0<x ⟩