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 HsumR: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n ∈ R.
Assume Hpos: Rlt 0 (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n).
Set s to be the term nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n.
Set invs to be the term recip_SNo_pos s.
We prove the intermediate claim HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsumR).
We prove the intermediate claim H0ltsS: 0 < s.
An exact proof term for the current goal is (RltE_lt 0 s Hpos).
We prove the intermediate claim HinvsR: invs ∈ R.
An exact proof term for the current goal is (real_recip_SNo_pos s HsumR H0ltsS).
We prove the intermediate claim HmulEq: mul_SNo s invs = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (mul_SNo (apply_fun (apply_fun e k) x) invs)) n.
An exact proof term for the current goal is (nat_primrec_add_mul_const_right X n e x invs HnO HxX HtermR HinvsR).
We prove the intermediate claim HinvR: mul_SNo s invs = 1.
An exact proof term for the current goal is (recip_SNo_pos_invR s HsS H0ltsS).
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HinvR.
∎