We will prove apply_fun flip_unit_interval 1 = 0.
We prove the intermediate claim H1I: 1 ∈ unit_interval.
An exact proof term for the current goal is one_in_unit_interval.
rewrite the current goal using (flip_unit_interval_apply 1 H1I) (from left to right).
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv 1 SNo_1).
∎