We will prove apply_fun double_minus_one_map_right_half 1 = 1.
rewrite the current goal using (double_minus_one_map_apply 1 one_in_unit_interval_right_half) (from left to right).
rewrite the current goal using (mul_SNo_oneR 2 SNo_2) (from left to right).
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (real_SNo (minus_SNo 1) Hm1R).
rewrite the current goal using add_SNo_1_1_2 (from right to left) at position 1.
rewrite the current goal using (add_SNo_assoc 1 1 (minus_SNo 1) SNo_1 SNo_1 Hm1S) (from right to left) at position 1.
We prove the intermediate claim Hinner: add_SNo 1 (minus_SNo 1) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv 1 SNo_1).
rewrite the current goal using Hinner (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right).
Use reflexivity.
∎