Let X and y be given.

Assume HX H1.

Apply H1 to the current goal.

Assume H.

Apply H to the current goal.

Assume H1a: y ∈ X.

Assume H1b: SNo y.

Assume H1c: ∀z ∈ X, SNo z → y ≤ z.

We will prove - y ∈ {- x|x ∈ X} ∧ SNo (- y) ∧ (∀z ∈ {- x|x ∈ X}, SNo z → z ≤ - y).

Apply and3I to the current goal.

Apply ReplI to the current goal.

An exact proof term for the current goal is H1a.

An exact proof term for the current goal is SNo_minus_SNo y H1b.

Let z be given.

Assume Hz1: z ∈ {- x|x ∈ X}.

Assume Hz2: SNo z.

Apply ReplE_impred X (λx ⇒ - x) z Hz1 to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume Hze: z = - x.

rewrite the current goal using Hze (from left to right).

We will prove - x ≤ - y.

Apply minus_SNo_Le_contra y x H1b (HX x Hx) to the current goal.

We will prove y ≤ x.

An exact proof term for the current goal is H1c x Hx (HX x Hx).

∎