Let t be given.
Assume HtR: t ∈ R.
Set num to be the term mul_SNo t t.
Set u to be the term add_SNo t (minus_SNo 1).
Set u2 to be the term mul_SNo u u.
Set den to be the term add_SNo num u2.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HnumS: SNo num.
An exact proof term for the current goal is (SNo_mul_SNo t t HtS HtS).
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim HuR: u ∈ R.
An exact proof term for the current goal is (real_add_SNo t HtR (minus_SNo 1) Hm1R).
We prove the intermediate claim HuS: SNo u.
An exact proof term for the current goal is (real_SNo u HuR).
We prove the intermediate claim Hu2S: SNo u2.
An exact proof term for the current goal is (SNo_mul_SNo u u HuS HuS).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo num u2 HnumS Hu2S).
We prove the intermediate claim H0le_num: 0 ≤ num.
An exact proof term for the current goal is (SNo_sqr_nonneg t HtS).
We prove the intermediate claim H0le_u2: 0 ≤ u2.
An exact proof term for the current goal is (SNo_sqr_nonneg u HuS).
We prove the intermediate claim H0le_den: 0 ≤ den.
We prove the intermediate claim H00le: add_SNo 0 0 ≤ add_SNo num u2.
An exact proof term for the current goal is (add_SNo_Le3 0 0 num u2 SNo_0 SNo_0 HnumS Hu2S H0le_num H0le_u2).
rewrite the current goal using (add_SNo_0R 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is H00le.
We prove the intermediate claim Hden_ne0: den ≠ 0.
Assume Hden0: den = 0.
We will prove False.
We prove the intermediate claim Hnum_le_den: num ≤ den.
An exact proof term for the current goal is (SNoLe_add_nonneg_right num u2 HnumS Hu2S H0le_u2).
We prove the intermediate claim Hu2_le_den: u2 ≤ den.
rewrite the current goal using (add_SNo_com num u2 HnumS Hu2S) (from left to right) at position 1.
An exact proof term for the current goal is (SNoLe_add_nonneg_right u2 num Hu2S HnumS H0le_num).
We prove the intermediate claim Hdenle0: den ≤ 0.
rewrite the current goal using Hden0 (from left to right) at position 1.
An exact proof term for the current goal is (SNoLe_ref 0).
We prove the intermediate claim Hnumle0: num ≤ 0.
An exact proof term for the current goal is (SNoLe_tra num den 0 HnumS HdenS SNo_0 Hnum_le_den Hdenle0).
We prove the intermediate claim Hu2le0: u2 ≤ 0.
An exact proof term for the current goal is (SNoLe_tra u2 den 0 Hu2S HdenS SNo_0 Hu2_le_den Hdenle0).
We prove the intermediate claim Hnum0: num = 0.
An exact proof term for the current goal is (SNoLe_antisym num 0 HnumS SNo_0 Hnumle0 H0le_num).
We prove the intermediate claim Hu20: u2 = 0.
An exact proof term for the current goal is (SNoLe_antisym u2 0 Hu2S SNo_0 Hu2le0 H0le_u2).
We prove the intermediate claim Ht0: t = 0.
We prove the intermediate claim Hcases: t = 0 ∨ 0 < mul_SNo t t.
An exact proof term for the current goal is (SNo_zero_or_sqr_pos t HtS).
Apply Hcases to the current goal.
Assume H0: t = 0.
An exact proof term for the current goal is H0.
Assume Hpos: 0 < mul_SNo t t.
We prove the intermediate claim Hpos0: 0 < 0.
rewrite the current goal using Hnum0 (from right to left) at position 2.
An exact proof term for the current goal is Hpos.
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) Hpos0) (t = 0)).
We prove the intermediate claim Hu0: u = 0.
We prove the intermediate claim Hcases: u = 0 ∨ 0 < mul_SNo u u.
An exact proof term for the current goal is (SNo_zero_or_sqr_pos u HuS).
Apply Hcases to the current goal.
Assume H0: u = 0.
An exact proof term for the current goal is H0.
Assume Hpos: 0 < mul_SNo u u.
We prove the intermediate claim Hpos0: 0 < 0.
rewrite the current goal using Hu20 (from right to left) at position 2.
An exact proof term for the current goal is Hpos.
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) Hpos0) (u = 0)).
We prove the intermediate claim Ht1: t = 1.
We prove the intermediate claim HtEq: add_SNo u 1 = t.
An exact proof term for the current goal is (add_SNo_minus_R2' t 1 HtS SNo_1).
rewrite the current goal using HtEq (from right to left).
rewrite the current goal using Hu0 (from left to right).
An exact proof term for the current goal is (add_SNo_0L 1 SNo_1).
We prove the intermediate claim H01: 0 = 1.
rewrite the current goal using Ht0 (from right to left) at position 1.
An exact proof term for the current goal is Ht1.
An exact proof term for the current goal is (neq_0_1 H01).
We prove the intermediate claim Hcases: 0 < den ∨ 0 = den.
An exact proof term for the current goal is (SNoLeE 0 den SNo_0 HdenS H0le_den).
Apply Hcases to the current goal.
Assume Hpos: 0 < den.
An exact proof term for the current goal is Hpos.
Assume Heq: 0 = den.
Apply FalseE to the current goal.
We prove the intermediate claim Hden0: den = 0.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (Hden_ne0 Hden0).
∎