Let p and q be given.
Assume HpR: p ∈ R.
Assume HqR: q ∈ R.
Assume HpNN: 0 ≤ p.
Assume HqNN: 0 ≤ q.
We prove the intermediate claim HpS: SNo p.
An exact proof term for the current goal is (real_SNo p HpR).
We prove the intermediate claim HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
We prove the intermediate claim HpplusqS: SNo (add_SNo p q).
An exact proof term for the current goal is (SNo_add_SNo p q HpS HqS).
Apply (xm (Rlt (add_SNo p q) 1)) to the current goal.
Assume Hlt: Rlt (add_SNo p q) 1.
rewrite the current goal using (If_i_1 (Rlt (add_SNo p q) 1) (add_SNo p q) 1 Hlt) (from left to right).
We prove the intermediate claim Hp1: Rlt p 1.
Apply (SNoLt_trichotomy_or_impred p 1 HpS SNo_1 (Rlt p 1)) to the current goal.
Assume Hpl: p < 1.
An exact proof term for the current goal is (RltI p 1 HpR real_1 Hpl).
Assume Hpeq: p = 1.
We prove the intermediate claim HsumS: SNo (add_SNo p q).
An exact proof term for the current goal is (real_SNo (add_SNo p q) (real_add_SNo p HpR q HqR)).
We prove the intermediate claim Hsumlt: add_SNo p q < 1.
An exact proof term for the current goal is (RltE_lt (add_SNo p q) 1 Hlt).
We prove the intermediate claim H1lesum: 1 ≤ add_SNo p q.
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le2 1 0 q SNo_1 SNo_0 HqS HqNN).
We prove the intermediate claim H11: 1 < 1.
An exact proof term for the current goal is (SNoLeLt_tra 1 (add_SNo p q) 1 SNo_1 HsumS SNo_1 H1lesum Hsumlt).
An exact proof term for the current goal is (FalseE ((SNoLt_irref 1) H11) (Rlt p 1)).
Assume H1lp: 1 < p.
We prove the intermediate claim H1lep: 1 ≤ p.
An exact proof term for the current goal is (SNoLtLe 1 p H1lp).
We prove the intermediate claim H1lesum: 1 ≤ add_SNo p q.
We prove the intermediate claim Hplepq: p ≤ add_SNo p q.
rewrite the current goal using (add_SNo_0R p HpS) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le2 p 0 q HpS SNo_0 HqS HqNN).
An exact proof term for the current goal is (SNoLe_tra 1 p (add_SNo p q) SNo_1 HpS (SNo_add_SNo p q HpS HqS) H1lep Hplepq).
We prove the intermediate claim Hsumlt: add_SNo p q < 1.
An exact proof term for the current goal is (RltE_lt (add_SNo p q) 1 Hlt).
We prove the intermediate claim H11: 1 < 1.
An exact proof term for the current goal is (SNoLeLt_tra 1 (add_SNo p q) 1 SNo_1 (SNo_add_SNo p q HpS HqS) SNo_1 H1lesum Hsumlt).
An exact proof term for the current goal is (FalseE ((SNoLt_irref 1) H11) (Rlt p 1)).
We prove the intermediate claim Hq1: Rlt q 1.
Apply (SNoLt_trichotomy_or_impred q 1 HqS SNo_1 (Rlt q 1)) to the current goal.
Assume Hql: q < 1.
An exact proof term for the current goal is (RltI q 1 HqR real_1 Hql).
Assume Hqeq: q = 1.
We prove the intermediate claim HsumS: SNo (add_SNo p q).
An exact proof term for the current goal is (real_SNo (add_SNo p q) (real_add_SNo p HpR q HqR)).
We prove the intermediate claim Hsumlt: add_SNo p q < 1.
An exact proof term for the current goal is (RltE_lt (add_SNo p q) 1 Hlt).
We prove the intermediate claim H1lesum: 1 ≤ add_SNo p q.
rewrite the current goal using Hqeq (from left to right).
rewrite the current goal using (add_SNo_com p 1 HpS SNo_1) (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le2 1 0 p SNo_1 SNo_0 HpS HpNN).
We prove the intermediate claim H11: 1 < 1.
An exact proof term for the current goal is (SNoLeLt_tra 1 (add_SNo p q) 1 SNo_1 HsumS SNo_1 H1lesum Hsumlt).
An exact proof term for the current goal is (FalseE ((SNoLt_irref 1) H11) (Rlt q 1)).
Assume H1lq: 1 < q.
We prove the intermediate claim H1leq: 1 ≤ q.
An exact proof term for the current goal is (SNoLtLe 1 q H1lq).
We prove the intermediate claim H1lesum: 1 ≤ add_SNo p q.
We prove the intermediate claim Hqlesum: q ≤ add_SNo p q.
rewrite the current goal using (add_SNo_com p q HpS HqS) (from left to right).
rewrite the current goal using (add_SNo_0R q HqS) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le2 q 0 p HqS SNo_0 HpS HpNN).
An exact proof term for the current goal is (SNoLe_tra 1 q (add_SNo p q) SNo_1 HqS (SNo_add_SNo p q HpS HqS) H1leq Hqlesum).
We prove the intermediate claim HsumS: SNo (add_SNo p q).
An exact proof term for the current goal is (SNo_add_SNo p q HpS HqS).
We prove the intermediate claim Hsumlt: add_SNo p q < 1.
An exact proof term for the current goal is (RltE_lt (add_SNo p q) 1 Hlt).
We prove the intermediate claim H11: 1 < 1.
An exact proof term for the current goal is (SNoLeLt_tra 1 (add_SNo p q) 1 SNo_1 HsumS SNo_1 H1lesum Hsumlt).
An exact proof term for the current goal is (FalseE ((SNoLt_irref 1) H11) (Rlt q 1)).
rewrite the current goal using (If_i_1 (Rlt p 1) p 1 Hp1) (from left to right).
rewrite the current goal using (If_i_1 (Rlt q 1) q 1 Hq1) (from left to right).
An exact proof term for the current goal is (SNoLe_ref (add_SNo p q)).
Assume Hnlt: ¬ (Rlt (add_SNo p q) 1).
rewrite the current goal using (If_i_0 (Rlt (add_SNo p q) 1) (add_SNo p q) 1 Hnlt) (from left to right).
Apply (xm (Rlt p 1)) to the current goal.
Assume Hp1: Rlt p 1.
rewrite the current goal using (If_i_1 (Rlt p 1) p 1 Hp1) (from left to right).
Apply (xm (Rlt q 1)) to the current goal.
Assume Hq1: Rlt q 1.
rewrite the current goal using (If_i_1 (Rlt q 1) q 1 Hq1) (from left to right).
We prove the intermediate claim H1le: 1 ≤ add_SNo p q.
Apply (SNoLt_trichotomy_or_impred (add_SNo p q) 1 HpplusqS SNo_1 (1 ≤ add_SNo p q)) to the current goal.
Assume Hslt: add_SNo p q < 1.
We prove the intermediate claim Hr: Rlt (add_SNo p q) 1.
An exact proof term for the current goal is (RltI (add_SNo p q) 1 (real_add_SNo p HpR q HqR) real_1 Hslt).
An exact proof term for the current goal is (FalseE (Hnlt Hr) (1 ≤ add_SNo p q)).
Assume Heq: add_SNo p q = 1.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SNoLe_ref 1).
Assume H1lt: 1 < add_SNo p q.
An exact proof term for the current goal is (SNoLtLe 1 (add_SNo p q) H1lt).
An exact proof term for the current goal is H1le.
Assume Hnq1: ¬ (Rlt q 1).
rewrite the current goal using (If_i_0 (Rlt q 1) q 1 Hnq1) (from left to right).
rewrite the current goal using (add_SNo_com p 1 HpS SNo_1) (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le2 1 0 p SNo_1 SNo_0 HpS HpNN).
Assume Hnp1: ¬ (Rlt p 1).
rewrite the current goal using (If_i_0 (Rlt p 1) p 1 Hnp1) (from left to right).
We prove the intermediate claim HclipS: SNo (If_i (Rlt q 1) q 1).
Apply (xm (Rlt q 1)) to the current goal.
Assume Hq1.
rewrite the current goal using (If_i_1 (Rlt q 1) q 1 Hq1) (from left to right).
An exact proof term for the current goal is HqS.
Assume Hnq1.
rewrite the current goal using (If_i_0 (Rlt q 1) q 1 Hnq1) (from left to right).
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim HclipNN: 0 ≤ If_i (Rlt q 1) q 1.
Apply (xm (Rlt q 1)) to the current goal.
Assume Hq1.
rewrite the current goal using (If_i_1 (Rlt q 1) q 1 Hq1) (from left to right).
An exact proof term for the current goal is HqNN.
Assume Hnq1.
rewrite the current goal using (If_i_0 (Rlt q 1) q 1 Hnq1) (from left to right).
An exact proof term for the current goal is (SNoLtLe 0 1 SNoLt_0_1).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from right to left) at position 1.
An exact proof term for the current goal is (add_SNo_Le2 1 0 (If_i (Rlt q 1) q 1) SNo_1 SNo_0 HclipS HclipNN).
∎