Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ 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 Habs: abs_SNo (add_SNo a (minus_SNo b)) = abs_SNo (add_SNo b (minus_SNo a)).
An exact proof term for the current goal is (abs_SNo_dist_swap a b HaS HbS).
We prove the intermediate claim Hab: R_bounded_distance a b = If_i (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1) (abs_SNo (add_SNo a (minus_SNo b))) 1.
Use reflexivity.
We prove the intermediate claim Hba: R_bounded_distance b a = If_i (Rlt (abs_SNo (add_SNo b (minus_SNo a))) 1) (abs_SNo (add_SNo b (minus_SNo a))) 1.
Use reflexivity.
rewrite the current goal using Hab (from left to right).
rewrite the current goal using Hba (from left to right).
Apply (xm (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1)) to the current goal.
Assume Hlt: Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1.
We prove the intermediate claim Hlt2: Rlt (abs_SNo (add_SNo b (minus_SNo a))) 1.
We will prove Rlt (abs_SNo (add_SNo b (minus_SNo a))) 1.
rewrite the current goal using Habs (from right to left).
An exact proof term for the current goal is Hlt.
rewrite the current goal using (If_i_1 (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1) (abs_SNo (add_SNo a (minus_SNo b))) 1 Hlt) (from left to right).
rewrite the current goal using (If_i_1 (Rlt (abs_SNo (add_SNo b (minus_SNo a))) 1) (abs_SNo (add_SNo b (minus_SNo a))) 1 Hlt2) (from left to right).
rewrite the current goal using Habs (from right to left).
Use reflexivity.
Assume Hnlt: ¬ (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1).
We prove the intermediate claim Hnlt2: ¬ (Rlt (abs_SNo (add_SNo b (minus_SNo a))) 1).
Assume Hlt2: Rlt (abs_SNo (add_SNo b (minus_SNo a))) 1.
We prove the intermediate claim Hlt1: Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1.
We will prove Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1.
rewrite the current goal using Habs (from left to right).
An exact proof term for the current goal is Hlt2.
An exact proof term for the current goal is (Hnlt Hlt1).
rewrite the current goal using (If_i_0 (Rlt (abs_SNo (add_SNo a (minus_SNo b))) 1) (abs_SNo (add_SNo a (minus_SNo b))) 1 Hnlt) (from left to right).
rewrite the current goal using (If_i_0 (Rlt (abs_SNo (add_SNo b (minus_SNo a))) 1) (abs_SNo (add_SNo b (minus_SNo a))) 1 Hnlt2) (from left to right).
Use reflexivity.
∎