Let p be given.
Assume HpB: p ∈ ordsq_B.
We will prove p ∈ ordered_square.
We prove the intermediate claim Hexn: ∃n ∈ ω ∖ {0}, p = (add_SNo 1 (minus_SNo (inv_nat n)),eps_ 1).
An exact proof term for the current goal is (ReplE (ω ∖ {0}) (λn0 : set ⇒ (add_SNo 1 (minus_SNo (inv_nat n0)),eps_ 1)) p HpB).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack.
Apply Hnpack to the current goal.
Assume HnIn Hpeq.
rewrite the current goal using Hpeq (from left to right).
We prove the intermediate claim HinvU: inv_nat n ∈ unit_interval.
An exact proof term for the current goal is (inv_nat_in_unit_interval n HnIn).
We prove the intermediate claim HflipI: apply_fun flip_unit_interval (inv_nat n) ∈ unit_interval.
An exact proof term for the current goal is (flip_unit_interval_function_on (inv_nat n) HinvU).
We prove the intermediate claim HflipEq: apply_fun flip_unit_interval (inv_nat n) = add_SNo 1 (minus_SNo (inv_nat n)).
An exact proof term for the current goal is (flip_unit_interval_apply (inv_nat n) HinvU).
We prove the intermediate claim HfirstU: add_SNo 1 (minus_SNo (inv_nat n)) ∈ unit_interval.
rewrite the current goal using HflipEq (from right to left).
An exact proof term for the current goal is HflipI.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval unit_interval (add_SNo 1 (minus_SNo (inv_nat n))) (eps_ 1) HfirstU eps_1_in_unit_interval).
∎