Add inversion lemmas for top-marker + bridges

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/Order.agda

@@ -156,6 +156,10 @@ infix 4 _<ᵇ_
 <ᵇ-inv-+Ωfin : ∀ {x y n} → bplus x y <ᵇ bOmega (fin n) → ⊥
 <ᵇ-inv-+Ωfin ()
 
+-- Inversion for the admitted top-marker bridge.
+<ᵇ-inv-+Ωω : ∀ {x y} → bplus x y <ᵇ bOmega ω → x <ᵇ bOmega ω
+<ᵇ-inv-+Ωω (<ᵇ-+ω x<ω) = x<ω
+
 ----------------------------------------------------------------------------
 -- WF-2 open-case inversions (ψ vs +)
 ----------------------------------------------------------------------------
@@ -169,6 +173,10 @@ infix 4 _<ᵇ_
 <ᵇ-inv-+ψfin : ∀ {x y n α} → bplus x y <ᵇ bpsi (fin n) α → ⊥
 <ᵇ-inv-+ψfin ()
 
+-- Inversion for the admitted top-marker bridge.
+<ᵇ-inv-+ψω : ∀ {x y α} → bplus x y <ᵇ bpsi ω α → x <ᵇ bpsi ω α
+<ᵇ-inv-+ψω (<ᵇ-+ψω x<ψω) = x<ψω
+
 ----------------------------------------------------------------------------
 -- Strict-below-ψ examples, for downstream ordering checks
 ----------------------------------------------------------------------------

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -62,8 +62,10 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-trans
   ; <ᵇ-inv-Ω+
   ; <ᵇ-inv-+Ωfin
+  ; <ᵇ-inv-+Ωω
   ; <ᵇ-inv-ψ+
   ; <ᵇ-inv-+ψfin
+  ; <ᵇ-inv-+ψω
   )
 
 open import Ordinal.Buchholz.Psi using

proofs/agda/Smoke.agda

@@ -189,8 +189,10 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-trans
   ; <ᵇ-inv-Ω+
   ; <ᵇ-inv-+Ωfin
+  ; <ᵇ-inv-+Ωω
   ; <ᵇ-inv-ψ+
   ; <ᵇ-inv-+ψfin
+  ; <ᵇ-inv-+ψω
   ; bzero<Ω0
   ; Ω0<Ω1
   ; Ω1<Ωω