Let X, n, e, x and k be given.
Assume HnO: n ∈ ω.
Assume HkIn: k ∈ n.
Assume HxX: x ∈ X.
Assume HtermR: ∀j : set, j ∈ n → apply_fun (apply_fun e j) x ∈ R.
Assume Hterm0: ∀j : set, j ∈ n → Rle 0 (apply_fun (apply_fun e j) x).
Assume HsumkR: nat_primrec 0 (λj acc : set ⇒ add_SNo acc (apply_fun (apply_fun e j) x)) k ∈ R.
Set step to be the term (λj acc : set ⇒ add_SNo acc (apply_fun (apply_fun e j) x)).
We prove the intermediate claim HkO: k ∈ ω.
An exact proof term for the current goal is (omega_TransSet n HnO k HkIn).
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (omega_nat_p k HkO).
We prove the intermediate claim HtermkR: apply_fun (apply_fun e k) x ∈ R.
An exact proof term for the current goal is (HtermR k HkIn).
We prove the intermediate claim Htermk0: Rle 0 (apply_fun (apply_fun e k) x).
An exact proof term for the current goal is (Hterm0 k HkIn).
rewrite the current goal using (nat_primrec_S 0 step k HkNat) (from left to right).
We prove the intermediate claim HsumkS: SNo (nat_primrec 0 step k).
An exact proof term for the current goal is (real_SNo (nat_primrec 0 step k) HsumkR).
We prove the intermediate claim HtermkS: SNo (apply_fun (apply_fun e k) x).
An exact proof term for the current goal is (real_SNo (apply_fun (apply_fun e k) x) HtermkR).
We prove the intermediate claim Hcomm: add_SNo (nat_primrec 0 step k) (apply_fun (apply_fun e k) x) = add_SNo (apply_fun (apply_fun e k) x) (nat_primrec 0 step k).
An exact proof term for the current goal is (add_SNo_com (nat_primrec 0 step k) (apply_fun (apply_fun e k) x) HsumkS HtermkS).
rewrite the current goal using Hcomm (from left to right).
An exact proof term for the current goal is (Rle_increase_by_nonneg_left (apply_fun (apply_fun e k) x) (nat_primrec 0 step k) HtermkR HsumkR Htermk0).
∎