Let n be given.
Assume Hn.
rewrite the current goal using
add_SNo_1_1_2 (from right to left) at position 1.
We prove the intermediate
claim L2n1:
nat_p (2 ^ n).
We prove the intermediate
claim L2n2:
ordinal (2 ^ n).
An exact proof term for the current goal is L2n1.
We prove the intermediate
claim L2n3:
SNo (2 ^ n).
An exact proof term for the current goal is L2n2.
We prove the intermediate
claim L2n2n1:
nat_p (2 ^ n + 2 ^ n).
An exact proof term for the current goal is L2n1.
An exact proof term for the current goal is L2n1.
We prove the intermediate
claim L2n2n2:
ordinal (2 ^ n + 2 ^ n).
An exact proof term for the current goal is L2n2n1.
We prove the intermediate
claim L2n2n3:
SNo (2 ^ n + 2 ^ n).
An exact proof term for the current goal is L2n2n2.
We prove the intermediate
claim L2npLt2n2n:
∀m, SNo m → m < 2 ^ n → 2 ^ n + m < 2 ^ n + 2 ^ n.
Let m be given.
Assume Hm H1.
An
exact proof term for the current goal is
add_SNo_Lt2 (2 ^ n) m (2 ^ n) L2n3 Hm L2n3 H1.
We prove the intermediate
claim L2nLt2n2n:
2 ^ n < 2 ^ n + 2 ^ n.
rewrite the current goal using
add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
Apply L2npLt2n2n 0 SNo_0 to the current goal.
Apply IHn to the current goal.
Let f be given.
Let x be given.
Assume Hx.
Assume Hx HxSn.
Let p be given.
Assume Hp.
We prove the intermediate
claim L2a:
n ∈ SNoLev x.
rewrite the current goal using HxSn (from left to right).
An
exact proof term for the current goal is
restr_SNoLev x Hx3 n L2a.
Apply Hp to the current goal.
An exact proof term for the current goal is Hx3.
An exact proof term for the current goal is HxSn.
Apply SepI to the current goal.
An
exact proof term for the current goal is
restr_SNo_ x Hx3 n L2a.
An exact proof term for the current goal is L2b.
An
exact proof term for the current goal is
restr_SNo x Hx3 n L2a.
An exact proof term for the current goal is L2b.
Let u be given.
Assume Hu.
Let p be given.
Assume Hp.
Apply L2 u Hu to the current goal.
We prove the intermediate
claim Lf1a:
f (u ∩ SNoElts_ n) ∈ 2 ^ n.
An
exact proof term for the current goal is
Hf1 (u ∩ SNoElts_ n) Hu1.
Apply Hp to the current goal.
An exact proof term for the current goal is Lf1b.
An exact proof term for the current goal is Lf1c.
An exact proof term for the current goal is Lf1c.
An exact proof term for the current goal is L2n2.
An exact proof term for the current goal is Lf1a.
Apply andI to the current goal.
Apply Lg to the current goal.
Let g be given.
Assume H.
Apply H to the current goal.
We use g to witness the existential quantifier.
Apply bijI to the current goal.
Let u be given.
We will
prove g u ∈ 2 ^ n + 2 ^ n.
Apply L2 u Hu to the current goal.
Apply Lf u Hu to the current goal.
Apply xm (n ∈ u) to the current goal.
rewrite the current goal using Hg1 u H1 (from left to right).
An
exact proof term for the current goal is
SNoLt_tra (f (u ∩ SNoElts_ n)) (2 ^ n) (2 ^ n + 2 ^ n) Lfu3 L2n3 L2n2n3 Lfu4 L2nLt2n2n.
rewrite the current goal using Hg2 u H1 (from left to right).
An
exact proof term for the current goal is
L2npLt2n2n (f (u ∩ SNoElts_ n)) Lfu3 Lfu4.
Let u be given.
Let v be given.
Apply L2 u Hu to the current goal.
Apply Lf u Hu to the current goal.
Apply L2 v Hv to the current goal.
Apply Lf v Hv to the current goal.
We prove the intermediate
claim LnLu:
n ∈ SNoLev u.
rewrite the current goal using Hu0b (from left to right).
We prove the intermediate
claim LnLv:
n ∈ SNoLev v.
rewrite the current goal using Hv0b (from left to right).
Apply xm (n ∈ u) to the current goal.
rewrite the current goal using Hg1 u H1 (from left to right).
Apply xm (n ∈ v) to the current goal.
rewrite the current goal using Hg1 v H2 (from left to right).
An
exact proof term for the current goal is
Hf2 (u ∩ SNoElts_ n) Hu1 (v ∩ SNoElts_ n) Hv1 Hguv.
Apply SNo_eq u v Hu0a Hv0a to the current goal.
rewrite the current goal using Hv0b (from left to right).
An exact proof term for the current goal is Hu0b.
rewrite the current goal using Hu0b (from left to right).
Let i be given.
Apply ordsuccE n i Hi to the current goal.
We will
prove i ∈ u ↔ i ∈ v.
An
exact proof term for the current goal is
restr_SNoEq u ?? n LnLu i H3.
rewrite the current goal using Luv (from left to right).
An
exact proof term for the current goal is
restr_SNoEq v ?? n LnLv i H3.
rewrite the current goal using H3 (from left to right).
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is H2.
Assume _.
An exact proof term for the current goal is H1.
rewrite the current goal using Hg2 v H2 (from left to right).
We will
prove 2 ^ n < 2 ^ n.
rewrite the current goal using
add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
rewrite the current goal using Hguv (from right to left).
An exact proof term for the current goal is Lfu4.
rewrite the current goal using Hg2 u H1 (from left to right).
Apply xm (n ∈ v) to the current goal.
rewrite the current goal using Hg1 v H2 (from left to right).
We will
prove 2 ^ n < 2 ^ n.
rewrite the current goal using
add_SNo_0R (2 ^ n) L2n3 (from right to left) at position 1.
rewrite the current goal using Hguv (from left to right).
An exact proof term for the current goal is Lfv4.
rewrite the current goal using Hg2 v H2 (from left to right).
Apply SNo_eq u v Hu0a Hv0a to the current goal.
rewrite the current goal using Hv0b (from left to right).
An exact proof term for the current goal is Hu0b.
rewrite the current goal using Hu0b (from left to right).
Let i be given.
Apply ordsuccE n i Hi to the current goal.
We will
prove i ∈ u ↔ i ∈ v.
An
exact proof term for the current goal is
restr_SNoEq u ?? n LnLu i H3.
rewrite the current goal using Luv (from left to right).
An
exact proof term for the current goal is
restr_SNoEq v ?? n LnLv i H3.
rewrite the current goal using H3 (from left to right).
Apply iffI to the current goal.
An exact proof term for the current goal is H1 H4.
An exact proof term for the current goal is H2 H4.
Let m be given.
We prove the intermediate
claim Lm1:
nat_p m.
An
exact proof term for the current goal is
nat_p_trans (2 ^ n + 2 ^ n) L2n2n1 m Hm.
We prove the intermediate
claim Lm2:
SNo m.
An
exact proof term for the current goal is
nat_p_SNo m Lm1.
Apply Hf3 m H1 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu3a Hu3b Hu3c Hu3d.
rewrite the current goal using Hu4 (from right to left).
rewrite the current goal using Hu4 (from right to left).
We use
(SNo_extend1 u) to
witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
nat_p_omega n Hn.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is Lu2.
rewrite the current goal using
Hg1 (SNo_extend1 u) Lu3 (from left to right).
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is Hu2.
Apply Hf3 (m + - 2 ^ n) H1 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu3a Hu3b Hu3c Hu3d.
rewrite the current goal using Hu4 (from right to left).
rewrite the current goal using Hu4 (from right to left).
We use
(SNo_extend0 u) to
witness the existential quantifier.
Apply andI to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
nat_p_omega n Hn.
rewrite the current goal using Hu4 (from right to left).
An exact proof term for the current goal is Lu2.
rewrite the current goal using
Hg2 (SNo_extend0 u) Lu3 (from left to right).
rewrite the current goal using Hu4 (from right to left) at position 2.
We will
prove 2 ^ n + f u = m.
rewrite the current goal using Hu2 (from left to right).
We will
prove 2 ^ n + (m + - 2 ^ n) = m.
We will
prove (m + - 2 ^ n) + 2 ^ n = m.
We will
prove m + (- 2 ^ n + 2 ^ n) = m.
An
exact proof term for the current goal is
add_SNo_0R m Lm2.
∎