We will prove apply_fun flip_unit_interval 0 = 1.
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 (flip_unit_interval_apply 0 H0I) (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
∎