Let M and x be given.
Assume HM: M ∈ R.
Assume HxR: x ∈ R.
Assume Hlx: Rlt (minus_SNo M) x.
Assume HxM: Rlt x M.
Assume HMAbs: Rlt M (Abs x).
We prove the intermediate claim HAbsR: Abs x ∈ R.
An exact proof term for the current goal is (RltE_right M (Abs x) HMAbs).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 False) to the current goal.
Assume Hxlt0: x < 0.
We prove the intermediate claim Habseq: Abs x = minus_SNo x.
An exact proof term for the current goal is (neg_abs_SNo x HxS Hxlt0).
We prove the intermediate claim HMltAbs: M < Abs x.
An exact proof term for the current goal is (RltE_lt M (Abs x) HMAbs).
We prove the intermediate claim HMltnegx: M < minus_SNo x.
rewrite the current goal using Habseq (from right to left).
An exact proof term for the current goal is HMltAbs.
We prove the intermediate claim Hlxs: minus_SNo M < x.
An exact proof term for the current goal is (RltE_lt (minus_SNo M) x Hlx).
We prove the intermediate claim HmR: minus_SNo M ∈ R.
An exact proof term for the current goal is (real_minus_SNo M HM).
We prove the intermediate claim HmS: SNo (minus_SNo M).
An exact proof term for the current goal is (real_SNo (minus_SNo M) HmR).
We prove the intermediate claim Hnegxlt: minus_SNo x < minus_SNo (minus_SNo M).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo M) x HmS HxS Hlxs).
We prove the intermediate claim Hminv: minus_SNo (minus_SNo M) = M.
An exact proof term for the current goal is (minus_SNo_invol M (real_SNo M HM)).
We prove the intermediate claim HnegxltM: minus_SNo x < M.
rewrite the current goal using Hminv (from right to left).
An exact proof term for the current goal is Hnegxlt.
We prove the intermediate claim HAbsltM: Abs x < M.
rewrite the current goal using Habseq (from left to right) at position 1.
An exact proof term for the current goal is HnegxltM.
We prove the intermediate claim HRltAbsM: Rlt (Abs x) M.
An exact proof term for the current goal is (RltI (Abs x) M HAbsR HM HAbsltM).
We prove the intermediate claim HMM: Rlt M M.
An exact proof term for the current goal is (Rlt_tra M (Abs x) M HMAbs HRltAbsM).
An exact proof term for the current goal is ((not_Rlt_refl M HM) HMM).
Assume Hxeq0: x = 0.
We prove the intermediate claim H0le0: 0 ≤ 0.
Apply (SNoLtLe_or 0 0 SNo_0 SNo_0 (0 ≤ 0)) to the current goal.
Assume H00: 0 < 0.
An exact proof term for the current goal is (SNoLtLe 0 0 H00).
Assume H.
An exact proof term for the current goal is H.
We prove the intermediate claim Habseq: Abs 0 = 0.
An exact proof term for the current goal is (nonneg_abs_SNo 0 H0le0).
We prove the intermediate claim Hx0M: Rlt 0 M.
rewrite the current goal using Hxeq0 (from right to left).
An exact proof term for the current goal is HxM.
We prove the intermediate claim HMlt0: Rlt M 0.
We prove the intermediate claim HAbsx0: Abs x = 0.
rewrite the current goal using Hxeq0 (from left to right) at position 1.
An exact proof term for the current goal is Habseq.
rewrite the current goal using HAbsx0 (from right to left).
An exact proof term for the current goal is HMAbs.
We prove the intermediate claim HMM: Rlt M M.
An exact proof term for the current goal is (Rlt_tra M 0 M HMlt0 Hx0M).
An exact proof term for the current goal is ((not_Rlt_refl M HM) HMM).
Assume H0ltx: 0 < x.
We prove the intermediate claim H0lex: 0 ≤ x.
An exact proof term for the current goal is (SNoLtLe 0 x H0ltx).
We prove the intermediate claim Habseq: Abs x = x.
An exact proof term for the current goal is (nonneg_abs_SNo x H0lex).
We prove the intermediate claim HMltAbs: M < Abs x.
An exact proof term for the current goal is (RltE_lt M (Abs x) HMAbs).
We prove the intermediate claim HMltx: M < x.
rewrite the current goal using Habseq (from right to left).
An exact proof term for the current goal is HMltAbs.
We prove the intermediate claim HxltM: x < M.
An exact proof term for the current goal is (RltE_lt x M HxM).
We prove the intermediate claim HRltMx: Rlt M x.
An exact proof term for the current goal is (RltI M x HM HxR HMltx).
We prove the intermediate claim HRltxM: Rlt x M.
An exact proof term for the current goal is HxM.
We prove the intermediate claim HMM: Rlt M M.
An exact proof term for the current goal is (Rlt_tra M x M HRltMx HRltxM).
An exact proof term for the current goal is ((not_Rlt_refl M HM) HMM).
∎