Let X be given.
Assume HX: ∀x ∈ X, SNo x.
Assume H1: finite X.
Assume H2: X ≠ 0.
Set X' to be the term {- x|x ∈ X}.
We prove the intermediate claim L1: ∀z ∈ X', SNo z.
Let z be given.
Assume Hz.
Apply ReplE_impred X (λx ⇒ - x) z Hz to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Assume Hzx: z = - x.
rewrite the current goal using Hzx (from left to right).
Apply SNo_minus_SNo to the current goal.
We will prove SNo x.
An exact proof term for the current goal is HX x Hx.
We prove the intermediate claim L2: finite X'.
Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Assume H3: equip X n.
We will prove ∃n ∈ ω, equip X' n.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
We will prove equip X' n.
Apply equip_tra X' X n to the current goal.
We will prove equip X' X.
Apply equip_sym to the current goal.
We will prove equip X X'.
We will prove ∃f : set → set, bij X X' f.
We use minus_SNo to witness the existential quantifier.
Apply bijI to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove - x ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
Let x be given.
Assume Hx.
Let x' be given.
Assume Hx'.
Assume Hxx': - x = - x'.
We will prove x = x'.
Use transitivity with - - x, and - - x'.
Use symmetry.
An exact proof term for the current goal is minus_SNo_invol x (HX x Hx).
Use f_equal.
An exact proof term for the current goal is Hxx'.
An exact proof term for the current goal is minus_SNo_invol x' (HX x' Hx').
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred X (λx ⇒ - x) w Hw to the current goal.
Let x be given.
Assume Hx.
Assume Hwx: w = - x.
We will prove ∃u ∈ X, - u = w.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx.
Use symmetry.
An exact proof term for the current goal is Hwx.
We will prove equip X n.
An exact proof term for the current goal is H3.
We prove the intermediate claim L3: X' ≠ 0.
Assume H1: X' = 0.
Apply H2 to the current goal.
We will prove X = 0.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx: x ∈ X.
Apply EmptyE (- x) to the current goal.
We will prove - x ∈ 0.
rewrite the current goal using H1 (from right to left).
Apply ReplI to the current goal.
An exact proof term for the current goal is Hx.
Apply finite_max_exists X' L1 L2 L3 to the current goal.
Let y be given.
Assume Hy: SNo_max_of X' y.
We use (- y) to witness the existential quantifier.
We will prove SNo_min_of X (- y).
An exact proof term for the current goal is minus_SNo_max_min' X y HX Hy.
∎