Let x and y be given.
Assume Hxy: Rle x y.
We will prove Rle (minus_SNo y) (minus_SNo x).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (RleE_left x y Hxy).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (RleE_right x y Hxy).
We prove the intermediate claim Hnxlt: ¬ (Rlt y x).
An exact proof term for the current goal is (RleE_nlt x y Hxy).
We prove the intermediate claim HmxR: minus_SNo x ∈ R.
An exact proof term for the current goal is (real_minus_SNo x HxR).
We prove the intermediate claim HmyR: minus_SNo y ∈ R.
An exact proof term for the current goal is (real_minus_SNo y HyR).
Apply (RleI (minus_SNo y) (minus_SNo x) HmyR HmxR) to the current goal.
Assume Hlt: Rlt (minus_SNo x) (minus_SNo y).
We prove the intermediate claim HltS: (minus_SNo x) < (minus_SNo y).
An exact proof term for the current goal is (RltE_lt (minus_SNo x) (minus_SNo y) Hlt).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim HmxS: SNo (minus_SNo x).
An exact proof term for the current goal is (SNo_minus_SNo x HxS).
We prove the intermediate claim HmyS: SNo (minus_SNo y).
An exact proof term for the current goal is (SNo_minus_SNo y HyS).
Apply (SNoLt_trichotomy_or_impred x y HxS HyS False) to the current goal.
Assume Hxly: x < y.
We prove the intermediate claim Hmyltmx: (minus_SNo y) < (minus_SNo x).
An exact proof term for the current goal is (minus_SNo_Lt_contra x y HxS HyS Hxly).
We prove the intermediate claim Hmxltmx: (minus_SNo x) < (minus_SNo x).
An exact proof term for the current goal is (SNoLt_tra (minus_SNo x) (minus_SNo y) (minus_SNo x) HmxS HmyS HmxS HltS Hmyltmx).
An exact proof term for the current goal is ((SNoLt_irref (minus_SNo x)) Hmxltmx).
Assume HxyEq: x = y.
We prove the intermediate claim HnegEq: minus_SNo y = minus_SNo x.
rewrite the current goal using HxyEq (from left to right).
Use reflexivity.
We prove the intermediate claim Hmxltmx: (minus_SNo x) < (minus_SNo x).
We will prove (minus_SNo x) < (minus_SNo x).
rewrite the current goal using HnegEq (from right to left) at position 2.
An exact proof term for the current goal is HltS.
An exact proof term for the current goal is ((SNoLt_irref (minus_SNo x)) Hmxltmx).
Assume Hyxlt: y < x.
We prove the intermediate claim HyxRlt: Rlt y x.
An exact proof term for the current goal is (RltI y x HyR HxR Hyxlt).
An exact proof term for the current goal is (Hnxlt HyxRlt).
∎