Let X be given.
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.
Let x be given.
rewrite the current goal using Hzx (from left to right).
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.
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.
We will
prove equip X' X.
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.
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'.
Use transitivity with
- - x, and
- - x'.
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.
Let x be given.
Assume Hx.
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.
An exact proof term for the current goal is H3.
We prove the intermediate
claim L3:
X' ≠ 0.
Apply H2 to the current goal.
Let x be given.
Apply EmptyE (- x) to the current goal.
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.
Let y be given.
We use
(- y) to
witness the existential quantifier.
∎