Let a be given.
Assume Ha.
Let b be given.
Assume Hb.
We prove the intermediate
claim LaS:
SNo a.
An
exact proof term for the current goal is
int_SNo a Ha.
We prove the intermediate
claim LbS:
SNo b.
An
exact proof term for the current goal is
int_SNo b Hb.
We prove the intermediate
claim L1:
∃c, ordinal c ∧ p c.
Let a' be given.
We prove the intermediate
claim La'N:
nat_p a'.
An exact proof term for the current goal is Ha'.
We prove the intermediate
claim La':
ordinal a'.
An exact proof term for the current goal is La'N.
We prove the intermediate
claim LSa'S:
SNo (ordsucc a').
An exact proof term for the current goal is La'N.
We use
ordsucc a' to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is La'.
Apply andI to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is Ha'.
We use
(- 1) to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_1.
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_0.
rewrite the current goal using
mul_SNo_zeroL b LbS (from left to right).
rewrite the current goal using
mul_SNo_oneL a LaS (from left to right).
rewrite the current goal using Haa' (from left to right).
Let b' be given.
We prove the intermediate
claim Lb'N:
nat_p b'.
An exact proof term for the current goal is Hb'.
We prove the intermediate
claim Lb':
ordinal b'.
An exact proof term for the current goal is Lb'N.
We prove the intermediate
claim LSb'S:
SNo (ordsucc b').
An exact proof term for the current goal is Lb'N.
We use
ordsucc b' to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lb'.
Apply andI to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is Hb'.
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_0.
We use
(- 1) to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_1.
rewrite the current goal using
mul_SNo_zeroL a LaS (from left to right).
rewrite the current goal using
mul_SNo_oneL b LbS (from left to right).
rewrite the current goal using Hbb' (from left to right).
Apply H1 to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
Let b' be given.
We prove the intermediate
claim Lb':
ordinal b'.
An exact proof term for the current goal is Hb'.
We use
ordsucc b' to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lb'.
Apply andI to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is Hb'.
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_0.
We use
1 to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_1.
rewrite the current goal using Hbb' (from right to left).
rewrite the current goal using
mul_SNo_zeroL a LaS (from left to right).
rewrite the current goal using
mul_SNo_oneL b LbS (from left to right).
An
exact proof term for the current goal is
add_SNo_0L b LbS.
Let a' be given.
We prove the intermediate
claim La':
ordinal a'.
An exact proof term for the current goal is Ha'.
We use
ordsucc a' to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is La'.
Apply andI to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is Ha'.
We use
1 to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_1.
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
nat_0.
rewrite the current goal using Haa' (from right to left).
rewrite the current goal using
mul_SNo_zeroL b LbS (from left to right).
rewrite the current goal using
mul_SNo_oneL a LaS (from left to right).
An
exact proof term for the current goal is
add_SNo_0R a LaS.
Apply L2 to the current goal.
Let c be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim LcS:
SNo c.
An
exact proof term for the current goal is
ordinal_SNo c Hco.
We use c to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hc1.
Let c' be given.
We prove the intermediate
claim Lc'Z:
c' ∈ int.
We prove the intermediate
claim Lc'S:
SNo c'.
An
exact proof term for the current goal is
int_SNo c' Lc'Z.
Apply SNoLtLe_or c' c Lc'S LcS to the current goal.
We prove the intermediate
claim Lc'N:
nat_p c'.
An exact proof term for the current goal is Hc'2.
We prove the intermediate
claim L3:
c' ∈ c.
Apply Hc2 c' L3 to the current goal.
We will prove p c'.
Apply andI to the current goal.
An exact proof term for the current goal is Hc'1.
An exact proof term for the current goal is Hc'2.
An exact proof term for the current goal is H2.
∎