Let t be given.
Assume HtR: t ∈ R.
We will prove apply_fun bounded_transform_phi t ∈ closed_interval (minus_SNo 1) 1.
Set f to be the term apply_fun bounded_transform_phi t.
We prove the intermediate claim HfR: f ∈ R.
An exact proof term for the current goal is (bounded_transform_phi_value_in_R t HtR).
We prove the intermediate claim HfDef: f = apply_fun bounded_transform_phi t.
Use reflexivity.
We prove the intermediate claim HphiDef: bounded_transform_phi = graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))).
Use reflexivity.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HabsR: abs_SNo t ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R t HtR).
We prove the intermediate claim HabsS: SNo (abs_SNo t).
An exact proof term for the current goal is (real_SNo (abs_SNo t) HabsR).
We prove the intermediate claim HdenS: SNo (add_SNo 1 (abs_SNo t)).
An exact proof term for the current goal is (SNo_add_SNo 1 (abs_SNo t) SNo_1 HabsS).
We prove the intermediate claim H0le_abs: 0 ≤ abs_SNo t.
An exact proof term for the current goal is (abs_SNo_nonneg t HtS).
We prove the intermediate claim HdenPos0: add_SNo 0 0 < add_SNo 1 (abs_SNo t).
An exact proof term for the current goal is (add_SNo_Lt3a 0 0 1 (abs_SNo t) SNo_0 SNo_0 SNo_1 HabsS SNoLt_0_1 H0le_abs).
We prove the intermediate claim HdenPos: 0 < add_SNo 1 (abs_SNo t).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is HdenPos0.
We prove the intermediate claim HfEq: f = div_SNo t (add_SNo 1 (abs_SNo t)).
rewrite the current goal using HfDef (from left to right).
rewrite the current goal using HphiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim HtLeAbs: t ≤ abs_SNo t.
An exact proof term for the current goal is (abs_SNo_upper_bound t HtS).
We prove the intermediate claim HtLtT1_raw: add_SNo t 0 < add_SNo t 1.
An exact proof term for the current goal is (add_SNo_Lt2 t 0 1 HtS SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim HtLtT1: t < add_SNo t 1.
rewrite the current goal using (add_SNo_0R t HtS) (from right to left) at position 1.
An exact proof term for the current goal is HtLtT1_raw.
We prove the intermediate claim Ht1LeAbs1: add_SNo t 1 ≤ add_SNo (abs_SNo t) 1.
An exact proof term for the current goal is (add_SNo_Le1 t 1 (abs_SNo t) HtS SNo_1 HabsS HtLeAbs).
We prove the intermediate claim Hab1S: SNo (add_SNo (abs_SNo t) 1).
An exact proof term for the current goal is (SNo_add_SNo (abs_SNo t) 1 HabsS SNo_1).
We prove the intermediate claim Ht1S: SNo (add_SNo t 1).
An exact proof term for the current goal is (SNo_add_SNo t 1 HtS SNo_1).
We prove the intermediate claim HtLtAbs1: t < add_SNo (abs_SNo t) 1.
An exact proof term for the current goal is (SNoLtLe_tra t (add_SNo t 1) (add_SNo (abs_SNo t) 1) HtS Ht1S Hab1S HtLtT1 Ht1LeAbs1).
We prove the intermediate claim Habs1EqDen: add_SNo (abs_SNo t) 1 = add_SNo 1 (abs_SNo t).
An exact proof term for the current goal is (add_SNo_com (abs_SNo t) 1 HabsS SNo_1).
We prove the intermediate claim HtLtDen: t < add_SNo 1 (abs_SNo t).
rewrite the current goal using Habs1EqDen (from right to left) at position 1.
An exact proof term for the current goal is HtLtAbs1.
We prove the intermediate claim HCI_def: closed_interval (minus_SNo 1) 1 = {x ∈ R|¬ (Rlt x (minus_SNo 1)) ∧ ¬ (Rlt 1 x)}.
Use reflexivity.
rewrite the current goal using HCI_def (from left to right).
Apply (SepI R (λx0 : set ⇒ ¬ (Rlt x0 (minus_SNo 1)) ∧ ¬ (Rlt 1 x0)) f HfR) to the current goal.
Apply andI to the current goal.
Assume Hlt: Rlt f (minus_SNo 1).
We will prove False.
We prove the intermediate claim HfLtM1: f < minus_SNo 1.
An exact proof term for the current goal is (RltE_lt f (minus_SNo 1) Hlt).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim HdivLt: div_SNo t (add_SNo 1 (abs_SNo t)) < minus_SNo 1.
rewrite the current goal using HfEq (from right to left).
An exact proof term for the current goal is HfLtM1.
We prove the intermediate claim HtLtM1den: t < mul_SNo (minus_SNo 1) (add_SNo 1 (abs_SNo t)).
An exact proof term for the current goal is (div_SNo_pos_LtL' t (add_SNo 1 (abs_SNo t)) (minus_SNo 1) HtS HdenS Hm1S HdenPos HdivLt).
We prove the intermediate claim Hm1denEq: mul_SNo (minus_SNo 1) (add_SNo 1 (abs_SNo t)) = minus_SNo (add_SNo 1 (abs_SNo t)).
rewrite the current goal using (mul_SNo_minus_distrL 1 (add_SNo 1 (abs_SNo t)) SNo_1 HdenS) (from left to right).
rewrite the current goal using (mul_SNo_oneL (add_SNo 1 (abs_SNo t)) HdenS) (from left to right).
Use reflexivity.
We prove the intermediate claim HtLtMden: t < minus_SNo (add_SNo 1 (abs_SNo t)).
rewrite the current goal using Hm1denEq (from right to left) at position 1.
An exact proof term for the current goal is HtLtM1den.
We prove the intermediate claim HabsLtAbs1_raw: add_SNo (abs_SNo t) 0 < add_SNo (abs_SNo t) 1.
An exact proof term for the current goal is (add_SNo_Lt2 (abs_SNo t) 0 1 HabsS SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim HabsLtAbs1: abs_SNo t < add_SNo (abs_SNo t) 1.
rewrite the current goal using (add_SNo_0R (abs_SNo t) HabsS) (from right to left) at position 1.
An exact proof term for the current goal is HabsLtAbs1_raw.
We prove the intermediate claim HabsLtDen: abs_SNo t < add_SNo 1 (abs_SNo t).
rewrite the current goal using Habs1EqDen (from right to left).
An exact proof term for the current goal is HabsLtAbs1.
We prove the intermediate claim HnegDenLtNegAbs: minus_SNo (add_SNo 1 (abs_SNo t)) < minus_SNo (abs_SNo t).
An exact proof term for the current goal is (minus_SNo_Lt_contra (abs_SNo t) (add_SNo 1 (abs_SNo t)) HabsS HdenS HabsLtDen).
We prove the intermediate claim HnegAbsLeT: minus_SNo (abs_SNo t) ≤ t.
An exact proof term for the current goal is (abs_SNo_lower_bound t HtS).
We prove the intermediate claim HmdenLtT: minus_SNo (add_SNo 1 (abs_SNo t)) < t.
We prove the intermediate claim HmabsS: SNo (minus_SNo (abs_SNo t)).
An exact proof term for the current goal is (SNo_minus_SNo (abs_SNo t) HabsS).
We prove the intermediate claim HmdenS: SNo (minus_SNo (add_SNo 1 (abs_SNo t))).
An exact proof term for the current goal is (SNo_minus_SNo (add_SNo 1 (abs_SNo t)) HdenS).
An exact proof term for the current goal is (SNoLtLe_tra (minus_SNo (add_SNo 1 (abs_SNo t))) (minus_SNo (abs_SNo t)) t HmdenS HmabsS HtS HnegDenLtNegAbs HnegAbsLeT).
We prove the intermediate claim Hbad: t < t.
An exact proof term for the current goal is (SNoLt_tra t (minus_SNo (add_SNo 1 (abs_SNo t))) t HtS (SNo_minus_SNo (add_SNo 1 (abs_SNo t)) HdenS) HtS HtLtMden HmdenLtT).
An exact proof term for the current goal is (FalseE ((SNoLt_irref t) Hbad) False).
Assume Hlt: Rlt 1 f.
We will prove False.
We prove the intermediate claim H1Lt: 1 < f.
An exact proof term for the current goal is (RltE_lt 1 f Hlt).
We prove the intermediate claim H1LtDiv: 1 < div_SNo t (add_SNo 1 (abs_SNo t)).
rewrite the current goal using HfEq (from right to left).
An exact proof term for the current goal is H1Lt.
We prove the intermediate claim HdenLtT_raw: mul_SNo 1 (add_SNo 1 (abs_SNo t)) < t.
An exact proof term for the current goal is (div_SNo_pos_LtR' t (add_SNo 1 (abs_SNo t)) 1 HtS HdenS SNo_1 HdenPos H1LtDiv).
We prove the intermediate claim HdenLtT: add_SNo 1 (abs_SNo t) < t.
rewrite the current goal using (mul_SNo_oneL (add_SNo 1 (abs_SNo t)) HdenS) (from right to left) at position 1.
An exact proof term for the current goal is HdenLtT_raw.
We prove the intermediate claim Hbad: add_SNo 1 (abs_SNo t) < add_SNo 1 (abs_SNo t).
An exact proof term for the current goal is (SNoLt_tra (add_SNo 1 (abs_SNo t)) t (add_SNo 1 (abs_SNo t)) HdenS HtS HdenS HdenLtT HtLtDen).
An exact proof term for the current goal is (FalseE ((SNoLt_irref (add_SNo 1 (abs_SNo t))) Hbad) False).
∎