Let x be given.
Assume Hx Hxpos.
Let g be given.
Assume Hg.
Set L to be the term ⋃k ∈ ωSNo_recipaux x g k 0.
Set R to be the term ⋃k ∈ ωSNo_recipaux x g k 1.
We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y).
We prove the intermediate claim L1: ∀k, nat_p k → (∀y ∈ SNo_recipaux x g k 0, SNo y ∧ x * y < 1) ∧ (∀y ∈ SNo_recipaux x g k 1, SNo y ∧ 1 < x * y).
An exact proof term for the current goal is SNo_recipaux_lem1 x Hx Hxpos g Hg.
Apply and3I to the current goal.
Let y be given.
Assume Hy.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x g k 0) y Hy to the current goal.
Let k be given.
Assume Hk.
Assume H1: y ∈ SNo_recipaux x g k 0.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 y H1 to the current goal.
Assume H3 _.
An exact proof term for the current goal is H3.
Let y be given.
Assume Hy.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x g k 1) y Hy to the current goal.
Let k be given.
Assume Hk.
Assume H1: y ∈ SNo_recipaux x g k 1.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume _ H2.
Apply H2 y H1 to the current goal.
Assume H3 _.
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw.
Let z be given.
Assume Hz.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x g k 0) w Hw to the current goal.
Let k be given.
Assume Hk.
Assume H1: w ∈ SNo_recipaux x g k 0.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume H3: SNo w.
Assume H4: x * w < 1.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x g k 1) z Hz to the current goal.
Let k' be given.
Assume Hk'.
Assume H5: z ∈ SNo_recipaux x g k' 1.
Apply L1 k' (omega_nat_p k' Hk') to the current goal.
Assume _ H6.
Apply H6 z H5 to the current goal.
Assume H7: SNo z.
Assume H8: 1 < x * z.
We will prove w < z.
Apply SNoLtLe_or w z H3 H7 to the current goal.
Assume H9: w < z.
An exact proof term for the current goal is H9.
Assume H9: z ≤ w.
We will prove False.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLt_tra 1 (x * z) 1 SNo_1 (SNo_mul_SNo x z Hx H7) SNo_1 H8 to the current goal.
We will prove x * z < 1.
Apply SNoLeLt_tra (x * z) (x * w) 1 (SNo_mul_SNo x z Hx H7) (SNo_mul_SNo x w Hx H3) SNo_1 to the current goal.
We will prove x * z ≤ x * w.
Apply nonneg_mul_SNo_Le x z w Hx (SNoLtLe 0 x Hxpos) H7 H3 H9 to the current goal.
We will prove x * w < 1.
An exact proof term for the current goal is H4.
∎