Let X, m, F, e, f0 and x be given.
Assume HmO: m ∈ ω.
Assume HxX: x ∈ X.
Assume Hbij: bijection (ordsucc m) F e.
Assume Hf0F: f0 ∈ F.
Assume HtermUI: ∀f : set, f ∈ F → apply_fun f x ∈ unit_interval.
Assume Hf00: apply_fun f0 x = 0.
We prove the intermediate claim Hmove: ∃e2 : set, bijection (ordsucc m) F e2 ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m) ∧ apply_fun e2 m = f0.
An exact proof term for the current goal is (nat_primrec_sum_bijection_move_value_to_last_unit_interval X m F e f0 x HmO HxX Hbij Hf0F HtermUI).
Apply Hmove to the current goal.
Let e2 be given.
Assume He2pack.
We prove the intermediate claim He2left: bijection (ordsucc m) F e2 ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m).
An exact proof term for the current goal is (andEL (bijection (ordsucc m) F e2 ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m)) (apply_fun e2 m = f0) He2pack).
We prove the intermediate claim Hbij2: bijection (ordsucc m) F e2.
An exact proof term for the current goal is (andEL (bijection (ordsucc m) F e2) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m)) He2left).
We prove the intermediate claim HsumEq: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m).
An exact proof term for the current goal is (andER (bijection (ordsucc m) F e2) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m)) He2left).
We prove the intermediate claim He2Last: apply_fun e2 m = f0.
An exact proof term for the current goal is (andER (bijection (ordsucc m) F e2 ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m)) (apply_fun e2 m = f0) He2pack).
We prove the intermediate claim Hlast0: apply_fun (apply_fun e2 m) x = 0.
rewrite the current goal using He2Last (from left to right).
An exact proof term for the current goal is Hf00.
We prove the intermediate claim He2fun: function_on e2 (ordsucc m) F.
An exact proof term for the current goal is (andEL (function_on e2 (ordsucc m) F) (∀y : set, y ∈ F → ∃k0 : set, k0 ∈ ordsucc m ∧ apply_fun e2 k0 = y ∧ (∀k' : set, k' ∈ ordsucc m → apply_fun e2 k' = y → k' = k0)) Hbij2).
We prove the intermediate claim HtermUI2: ∀k : set, k ∈ ordsucc m → apply_fun (apply_fun e2 k) x ∈ unit_interval.
Let k be given.
Assume HkDom: k ∈ ordsucc m.
An exact proof term for the current goal is (HtermUI (apply_fun e2 k) (He2fun k HkDom)).
We prove the intermediate claim Hdrop: bijection m (F ∖ {apply_fun e2 m}) e2 ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) m.
An exact proof term for the current goal is (nat_primrec_sum_drop_last_zero_bijection_unit_interval X m F e2 x HmO HxX HtermUI2 Hlast0 Hbij2).
We prove the intermediate claim HbijDrop: bijection m (F ∖ {apply_fun e2 m}) e2.
An exact proof term for the current goal is (andEL (bijection m (F ∖ {apply_fun e2 m}) e2) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) m) Hdrop).
We prove the intermediate claim HsumDrop: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) m.
An exact proof term for the current goal is (andER (bijection m (F ∖ {apply_fun e2 m}) e2) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m) = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) m) Hdrop).
We use e2 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HbijDrop2: bijection m (F ∖ {f0}) e2.
rewrite the current goal using He2Last (from right to left) at position 1.
An exact proof term for the current goal is HbijDrop.
An exact proof term for the current goal is HbijDrop2.
An exact proof term for the current goal is (eq_i_tra (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m)) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) (ordsucc m)) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e2 k) x)) m) HsumEq HsumDrop).
∎