Let f and n be given.
Assume Hf: f ∈ real_sequences.
Assume HnO: n ∈ ω.
We prove the intermediate claim Hfpack: total_function_on f ω R ∧ functional_graph f.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω R)) (λf0 : set ⇒ total_function_on f0 ω R ∧ functional_graph f0) f Hf).
We prove the intermediate claim Htotf: total_function_on f ω R.
An exact proof term for the current goal is (andEL (total_function_on f ω R) (functional_graph f) Hfpack).
We prove the intermediate claim HfnR: apply_fun f n ∈ R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f ω R n Htotf HnO).
We prove the intermediate claim HfnS: SNo (apply_fun f n).
An exact proof term for the current goal is (real_SNo (apply_fun f n) HfnR).
Set t to be the term add_SNo (apply_fun f n) (minus_SNo (apply_fun f n)).
We prove the intermediate claim Ht0: t = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv (apply_fun f n) HfnS).
We prove the intermediate claim H0le0: 0 ≤ 0.
An exact proof term for the current goal is (SNoLe_ref 0).
We prove the intermediate claim Habseq: abs_SNo 0 = 0.
An exact proof term for the current goal is (nonneg_abs_SNo 0 H0le0).
We prove the intermediate claim Habs0: abs_SNo t = 0.
rewrite the current goal using Ht0 (from left to right).
An exact proof term for the current goal is Habseq.
We prove the intermediate claim HdefAbs: Romega_coord_abs_diff f f n = abs_SNo t.
Use reflexivity.
We prove the intermediate claim HdefClip: Romega_coord_clipped_diff f f n = If_i (Rlt (Romega_coord_abs_diff f f n) 1) (Romega_coord_abs_diff f f n) 1.
Use reflexivity.
rewrite the current goal using HdefClip (from left to right).
rewrite the current goal using HdefAbs (from left to right).
rewrite the current goal using Habs0 (from left to right).
rewrite the current goal using (If_i_1 (Rlt 0 1) 0 1 Rlt_0_1) (from left to right).
Use reflexivity.
∎