Let J, f and g be given.
Assume Hf: f ∈ power_real J.
Assume Hg: g ∈ power_real J.
Set A to be the term power_real_clipped_diffs J f g.
Set B to be the term power_real_clipped_diffs J g f.
Apply set_ext to the current goal.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ B.
Apply (ReplE_impred J (λj : set ⇒ power_real_coord_clipped_diff f g j) a HaA (a ∈ B)) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Haj: a = power_real_coord_clipped_diff f g j.
rewrite the current goal using Haj (from left to right).
We prove the intermediate claim HfjR: apply_fun f j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J f j HjJ Hf).
We prove the intermediate claim HgjR: apply_fun g j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J g j HjJ Hg).
We prove the intermediate claim Hdef1: power_real_coord_clipped_diff f g j = R_bounded_distance (apply_fun f j) (apply_fun g j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J f g j HjJ Hf Hg).
We prove the intermediate claim Hdef2: power_real_coord_clipped_diff g f j = R_bounded_distance (apply_fun g j) (apply_fun f j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J g f j HjJ Hg Hf).
rewrite the current goal using Hdef1 (from left to right).
rewrite the current goal using (R_bounded_distance_sym (apply_fun f j) (apply_fun g j) HfjR HgjR) (from left to right).
rewrite the current goal using Hdef2 (from right to left).
An exact proof term for the current goal is (ReplI J (λj0 : set ⇒ power_real_coord_clipped_diff g f j0) j HjJ).
Let a be given.
Assume HaB: a ∈ B.
We will prove a ∈ A.
Apply (ReplE_impred J (λj : set ⇒ power_real_coord_clipped_diff g f j) a HaB (a ∈ A)) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Haj: a = power_real_coord_clipped_diff g f j.
rewrite the current goal using Haj (from left to right).
We prove the intermediate claim HfjR: apply_fun f j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J f j HjJ Hf).
We prove the intermediate claim HgjR: apply_fun g j ∈ R.
An exact proof term for the current goal is (power_real_coord_in_R J g j HjJ Hg).
We prove the intermediate claim Hdef1: power_real_coord_clipped_diff g f j = R_bounded_distance (apply_fun g j) (apply_fun f j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J g f j HjJ Hg Hf).
We prove the intermediate claim Hdef2: power_real_coord_clipped_diff f g j = R_bounded_distance (apply_fun f j) (apply_fun g j).
An exact proof term for the current goal is (power_real_coord_clipped_diff_eq_R_bounded_distance J f g j HjJ Hf Hg).
rewrite the current goal using Hdef1 (from left to right).
rewrite the current goal using (R_bounded_distance_sym (apply_fun g j) (apply_fun f j) HgjR HfjR) (from left to right).
rewrite the current goal using Hdef2 (from right to left).
An exact proof term for the current goal is (ReplI J (λj0 : set ⇒ power_real_coord_clipped_diff f g j0) j HjJ).
∎