Let X, n, F, e, i and x be given.
Assume HnO: n ∈ ω.
Assume HiN: i ∈ n.
Assume HsiN: ordsucc i ∈ n.
Assume HxX: x ∈ X.
Assume Hbij: bijection n F e.
Assume HtermUI: ∀k : set, k ∈ n → apply_fun (apply_fun e k) x ∈ unit_interval.
Assume Hzero: apply_fun (apply_fun e i) x = 0.
We use (swap_adjacent e i n) to witness the existential quantifier.
Apply andI to the current goal.
We will prove (swap_adjacent e i n = swap_adjacent e i n ∧ bijection n F (swap_adjacent e i n)) ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e i n) k) x)) n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n.
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
We prove the intermediate claim Hpair: bijection n F (swap_adjacent e i n) ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e i n) k) x)) n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n.
An exact proof term for the current goal is (nat_primrec_sum_swap_adjacent_bijection_unit_interval X n F e i x HnO HiN HsiN HxX Hbij HtermUI).
An exact proof term for the current goal is (andEL (bijection n F (swap_adjacent e i n)) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e i n) k) x)) n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n) Hpair).
We prove the intermediate claim Hpair: bijection n F (swap_adjacent e i n) ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e i n) k) x)) n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n.
An exact proof term for the current goal is (nat_primrec_sum_swap_adjacent_bijection_unit_interval X n F e i x HnO HiN HsiN HxX Hbij HtermUI).
An exact proof term for the current goal is (andER (bijection n F (swap_adjacent e i n)) (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e i n) k) x)) n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n) Hpair).
We prove the intermediate claim Happ: apply_fun (swap_adjacent e i n) (ordsucc i) = apply_fun e i.
An exact proof term for the current goal is (swap_adjacent_at_succ e i n HsiN).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is Hzero.
∎