Let X, n, e and x be given.
Assume HnO: n ∈ ω.
Assume HxX: x ∈ X.
Assume HtermR: ∀k : set, k ∈ n → apply_fun (apply_fun e k) x ∈ R.
Assume Hterm0: ∀k : set, k ∈ n → Rle 0 (apply_fun (apply_fun e k) x).
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)).
Set P to be the term (λm : set ⇒ m ∈ ordsucc n → nat_primrec 0 step m ∈ R ∧ Rle 0 (nat_primrec 0 step m)).
We prove the intermediate claim HP0: P 0.
Assume H0: 0 ∈ ordsucc n.
rewrite the current goal using (nat_primrec_0 0 step) (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is (Rle_refl 0 real_0).
We prove the intermediate claim HPS: ∀m : set, nat_p m → P m → P (ordsucc m).
Let m be given.
Assume HmNat: nat_p m.
Assume IH: P m.
Assume HmS: ordsucc m ∈ ordsucc n.
We prove the intermediate claim Hsub: ordsucc m ⊆ n.
An exact proof term for the current goal is (nat_ordsucc_trans n HnNat (ordsucc m) HmS).
We prove the intermediate claim HmInN: m ∈ n.
An exact proof term for the current goal is (Hsub m (ordsuccI2 m)).
We prove the intermediate claim HmInSuccN: m ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n m HmInN).
We prove the intermediate claim HIH: nat_primrec 0 step m ∈ R ∧ Rle 0 (nat_primrec 0 step m).
An exact proof term for the current goal is (IH HmInSuccN).
We prove the intermediate claim HsumR: nat_primrec 0 step m ∈ R.
An exact proof term for the current goal is (andEL (nat_primrec 0 step m ∈ R) (Rle 0 (nat_primrec 0 step m)) HIH).
We prove the intermediate claim Hsum0: Rle 0 (nat_primrec 0 step m).
An exact proof term for the current goal is (andER (nat_primrec 0 step m ∈ R) (Rle 0 (nat_primrec 0 step m)) HIH).
We prove the intermediate claim HtermRm: apply_fun (apply_fun e m) x ∈ R.
An exact proof term for the current goal is (HtermR m HmInN).
We prove the intermediate claim Hterm0m: Rle 0 (apply_fun (apply_fun e m) x).
An exact proof term for the current goal is (Hterm0 m HmInN).
rewrite the current goal using (nat_primrec_S 0 step m HmNat) (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is (real_add_SNo (nat_primrec 0 step m) HsumR (apply_fun (apply_fun e m) x) HtermRm).
We prove the intermediate claim HaccS: SNo (nat_primrec 0 step m).
An exact proof term for the current goal is (real_SNo (nat_primrec 0 step m) HsumR).
We prove the intermediate claim HaccLe: Rle (nat_primrec 0 step m) (add_SNo (nat_primrec 0 step m) (apply_fun (apply_fun e m) x)).
We will prove Rle (nat_primrec 0 step m) (add_SNo (nat_primrec 0 step m) (apply_fun (apply_fun e m) x)).
rewrite the current goal using (add_SNo_0R (nat_primrec 0 step m) HaccS) (from right to left) at position 1.
An exact proof term for the current goal is (Rle_add_SNo_2 (nat_primrec 0 step m) 0 (apply_fun (apply_fun e m) x) HsumR real_0 HtermRm Hterm0m).
An exact proof term for the current goal is (Rle_tra 0 (nat_primrec 0 step m) (add_SNo (nat_primrec 0 step m) (apply_fun (apply_fun e m) x)) Hsum0 HaccLe).
We prove the intermediate claim HPn: P n.
An exact proof term for the current goal is (nat_ind P HP0 HPS n HnNat).
We prove the intermediate claim HnIn: n ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI2 n).
An exact proof term for the current goal is (HPn HnIn).
∎