Let X, n, e and x be given.
Assume HnO: n ∈ ω.
Assume HxX: x ∈ X.
Assume HtermUI: ∀k : set, k ∈ ordsucc n → apply_fun (apply_fun e k) x ∈ unit_interval.
Assume Hlast0: apply_fun (apply_fun e n) x = 0.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
Set step to be the term (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)).
rewrite the current goal using (nat_primrec_S 0 step n HnNat) (from left to right).
rewrite the current goal using Hlast0 (from left to right).
Set acc to be the term nat_primrec 0 step n.
We prove the intermediate claim HaccR: acc ∈ R.
We prove the intermediate claim HtermR: ∀k : set, k ∈ n → apply_fun (apply_fun e k) x ∈ R.
Let k be given.
Assume HkN: k ∈ n.
We prove the intermediate claim HkDom: k ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n k HkN).
An exact proof term for the current goal is (unit_interval_sub_R (apply_fun (apply_fun e k) x) (HtermUI k HkDom)).
We prove the intermediate claim Hterm0: ∀k : set, k ∈ n → Rle 0 (apply_fun (apply_fun e k) x).
Let k be given.
Assume HkN: k ∈ n.
We prove the intermediate claim HkDom: k ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n k HkN).
An exact proof term for the current goal is (unit_interval_Rle0 (apply_fun (apply_fun e k) x) (HtermUI k HkDom)).
An exact proof term for the current goal is (andEL (nat_primrec 0 step n ∈ R) (Rle 0 (nat_primrec 0 step n)) (nat_primrec_sum_Rle0_of_Rle0_terms X n e x HnO HxX HtermR Hterm0)).
We prove the intermediate claim HaccS: SNo acc.
An exact proof term for the current goal is (real_SNo acc HaccR).
rewrite the current goal using (add_SNo_0R acc HaccS) (from left to right).
Use reflexivity.
∎