Let t be given.
Assume Ht: t ∈ unit_interval.
We will prove apply_fun flip_unit_interval t ∈ R.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R t Ht).
We prove the intermediate claim HmR: minus_SNo t ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
We prove the intermediate claim HaddR: add_SNo 1 (minus_SNo t) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo t) HmR).
rewrite the current goal using (flip_unit_interval_apply t Ht) (from left to right).
An exact proof term for the current goal is HaddR.
∎