Let J, f, g and j be given.
Assume HjJ: j ∈ J.
Assume Hf: f ∈ power_real J.
Assume Hg: g ∈ power_real J.
We will prove power_real_coord_clipped_diff f g j = R_bounded_distance (apply_fun f j) (apply_fun g j).
We prove the intermediate claim Hdef1: power_real_coord_clipped_diff f g j = If_i (Rlt (power_real_coord_abs_diff f g j) 1) (power_real_coord_abs_diff f g j) 1.
Use reflexivity.
We prove the intermediate claim Hdef2: power_real_coord_abs_diff f g j = abs_SNo (add_SNo (apply_fun f j) (minus_SNo (apply_fun g j))).
Use reflexivity.
We prove the intermediate claim Hdef3: R_bounded_distance (apply_fun f j) (apply_fun g j) = If_i (Rlt (abs_SNo (add_SNo (apply_fun f j) (minus_SNo (apply_fun g j)))) 1) (abs_SNo (add_SNo (apply_fun f j) (minus_SNo (apply_fun g j)))) 1.
Use reflexivity.
rewrite the current goal using Hdef1 (from left to right).
rewrite the current goal using Hdef2 (from left to right).
rewrite the current goal using Hdef3 (from left to right).
Use reflexivity.
∎