Let a, b and c be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
Set tab to be the term add_SNo a (minus_SNo b).
Set tbc to be the term add_SNo b (minus_SNo c).
Set tac to be the term add_SNo a (minus_SNo c).
We prove the intermediate claim HmbR: minus_SNo b ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
We prove the intermediate claim HmcR: minus_SNo c ∈ R.
An exact proof term for the current goal is (real_minus_SNo c HcR).
We prove the intermediate claim HtabR: tab ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR (minus_SNo b) HmbR).
We prove the intermediate claim HtbcR: tbc ∈ R.
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo c) HmcR).
We prove the intermediate claim HtacR: tac ∈ R.
An exact proof term for the current goal is (real_add_SNo a HaR (minus_SNo c) HmcR).
We prove the intermediate claim HtabS: SNo tab.
An exact proof term for the current goal is (real_SNo tab HtabR).
We prove the intermediate claim HtbcS: SNo tbc.
An exact proof term for the current goal is (real_SNo tbc HtbcR).
We prove the intermediate claim HtacS: SNo tac.
An exact proof term for the current goal is (real_SNo tac HtacR).
Set pab to be the term abs_SNo tab.
Set pbc to be the term abs_SNo tbc.
Set pac to be the term abs_SNo tac.
We prove the intermediate claim HpabR: pab ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R tab HtabR).
We prove the intermediate claim HpbcR: pbc ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R tbc HtbcR).
We prove the intermediate claim HpacR: pac ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R tac HtacR).
We prove the intermediate claim HpabS: SNo pab.
An exact proof term for the current goal is (real_SNo pab HpabR).
We prove the intermediate claim HpbcS: SNo pbc.
An exact proof term for the current goal is (real_SNo pbc HpbcR).
We prove the intermediate claim HpacS: SNo pac.
An exact proof term for the current goal is (real_SNo pac HpacR).
We prove the intermediate claim HpabNN: 0 ≤ pab.
An exact proof term for the current goal is (abs_SNo_nonneg tab HtabS).
We prove the intermediate claim HpbcNN: 0 ≤ pbc.
An exact proof term for the current goal is (abs_SNo_nonneg tbc HtbcS).
We prove the intermediate claim HabsTri: pac ≤ add_SNo pab pbc.
An exact proof term for the current goal is (abs_SNo_triangle a b c HaS HbS HcS).
We prove the intermediate claim Hmono: If_i (Rlt pac 1) pac 1 ≤ If_i (Rlt (add_SNo pab pbc) 1) (add_SNo pab pbc) 1.
An exact proof term for the current goal is (Rclip_mono pac (add_SNo pab pbc) HpacR (real_add_SNo pab HpabR pbc HpbcR) HabsTri).
We prove the intermediate claim Hsub: If_i (Rlt (add_SNo pab pbc) 1) (add_SNo pab pbc) 1 ≤ add_SNo (If_i (Rlt pab 1) pab 1) (If_i (Rlt pbc 1) pbc 1).
An exact proof term for the current goal is (Rclip_subadd_nonneg pab pbc HpabR HpbcR HpabNN HpbcNN).
We prove the intermediate claim HdefAC: R_bounded_distance a c = If_i (Rlt pac 1) pac 1.
Use reflexivity.
We prove the intermediate claim HdefAB: R_bounded_distance a b = If_i (Rlt pab 1) pab 1.
Use reflexivity.
We prove the intermediate claim HdefBC: R_bounded_distance b c = If_i (Rlt pbc 1) pbc 1.
Use reflexivity.
rewrite the current goal using HdefAC (from left to right).
rewrite the current goal using HdefAB (from left to right).
rewrite the current goal using HdefBC (from left to right).
An exact proof term for the current goal is (SNoLe_tra (If_i (Rlt pac 1) pac 1) (If_i (Rlt (add_SNo pab pbc) 1) (add_SNo pab pbc) 1) (add_SNo (If_i (Rlt pab 1) pab 1) (If_i (Rlt pbc 1) pbc 1)) (SNo_If_i (Rlt pac 1) pac 1 HpacS SNo_1) (SNo_If_i (Rlt (add_SNo pab pbc) 1) (add_SNo pab pbc) 1 (SNo_add_SNo pab pbc HpabS HpbcS) SNo_1) (SNo_add_SNo (If_i (Rlt pab 1) pab 1) (If_i (Rlt pbc 1) pbc 1) (SNo_If_i (Rlt pab 1) pab 1 HpabS SNo_1) (SNo_If_i (Rlt pbc 1) pbc 1 HpbcS SNo_1)) Hmono Hsub).
∎