We will prove apply_fun double_map_left_half 0 = 0.

We prove the intermediate claim H0I: 0 ∈ unit_interval.

An exact proof term for the current goal is zero_in_unit_interval.

rewrite the current goal using (double_map_apply 0 zero_in_unit_interval_left_half) (from left to right).

rewrite the current goal using (mul_SNo_zeroR 2 SNo_2) (from left to right).

Use reflexivity.

∎