Let b and x be given.
Assume Hb: b ∈ rectangular_regions.
Assume HxE: x ∈ EuclidPlane.
Assume Hxb: x ∈ b.
We prove the intermediate claim HbPred: ∃a b0 c d0 : set, a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0 ∧ Rlt c d0 ∧ b = {p ∈ EuclidPlane|∃x1 y1 : set, p = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b0 ∧ Rlt c y1 ∧ Rlt y1 d0}.
An exact proof term for the current goal is (SepE2 (𝒫 EuclidPlane) (λU0 : set ⇒ ∃a0 b0 c0 d0 : set, a0 ∈ R ∧ b0 ∈ R ∧ c0 ∈ R ∧ d0 ∈ R ∧ Rlt a0 b0 ∧ Rlt c0 d0 ∧ U0 = {p ∈ EuclidPlane|∃x1 y1 : set, p = (x1,y1) ∧ Rlt a0 x1 ∧ Rlt x1 b0 ∧ Rlt c0 y1 ∧ Rlt y1 d0}) b Hb).
Apply HbPred to the current goal.
Let a be given.
Assume HbPred2.
Apply HbPred2 to the current goal.
Let b0 be given.
Assume HbPred3.
Apply HbPred3 to the current goal.
Let c be given.
Assume HbPred4.
Apply HbPred4 to the current goal.
Let d0 be given.
Assume Habcd.
Set Rect to be the term {p ∈ EuclidPlane|∃x1 y1 : set, p = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b0 ∧ Rlt c y1 ∧ Rlt y1 d0}.
We prove the intermediate claim HbEq: b = Rect.
An exact proof term for the current goal is (andER (a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0 ∧ Rlt c d0) (b = Rect) Habcd).
We prove the intermediate claim HabcdLeft: a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0 ∧ Rlt c d0.
An exact proof term for the current goal is (andEL (a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0 ∧ Rlt c d0) (b = Rect) Habcd).
We prove the intermediate claim Hcd: Rlt c d0.
An exact proof term for the current goal is (andER (a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0) (Rlt c d0) HabcdLeft).
We prove the intermediate claim HabcdLeft2: a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0.
An exact proof term for the current goal is (andEL (a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R ∧ Rlt a b0) (Rlt c d0) HabcdLeft).
We prove the intermediate claim Hab: Rlt a b0.
An exact proof term for the current goal is (andER (a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R) (Rlt a b0) HabcdLeft2).
We prove the intermediate claim HabcdLeft3: a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R ∧ b0 ∈ R ∧ c ∈ R ∧ d0 ∈ R) (Rlt a b0) HabcdLeft2).
We prove the intermediate claim Hd0R: d0 ∈ R.
An exact proof term for the current goal is (andER (a ∈ R ∧ b0 ∈ R ∧ c ∈ R) (d0 ∈ R) HabcdLeft3).
We prove the intermediate claim HabcdLeft4: a ∈ R ∧ b0 ∈ R ∧ c ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R ∧ b0 ∈ R ∧ c ∈ R) (d0 ∈ R) HabcdLeft3).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andER (a ∈ R ∧ b0 ∈ R) (c ∈ R) HabcdLeft4).
We prove the intermediate claim HabR: a ∈ R ∧ b0 ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R ∧ b0 ∈ R) (c ∈ R) HabcdLeft4).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (b0 ∈ R) HabR).
We prove the intermediate claim Hb0R: b0 ∈ R.
An exact proof term for the current goal is (andER (a ∈ R) (b0 ∈ R) HabR).
We prove the intermediate claim HxRect: x ∈ Rect.
We will prove x ∈ Rect.
rewrite the current goal using HbEq (from right to left).
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HxRectPred: ∃x0 y0 : set, x = (x0,y0) ∧ Rlt a x0 ∧ Rlt x0 b0 ∧ Rlt c y0 ∧ Rlt y0 d0.
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ ∃x0 y0 : set, p0 = (x0,y0) ∧ Rlt a x0 ∧ Rlt x0 b0 ∧ Rlt c y0 ∧ Rlt y0 d0) x HxRect).
Apply HxRectPred to the current goal.
Let x0 be given.
Assume HxRectPred2.
Apply HxRectPred2 to the current goal.
Let y0 be given.
Assume Hxy0.
We prove the intermediate claim Hy0d0: Rlt y0 d0.
An exact proof term for the current goal is (andER (((x = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b0) ∧ Rlt c y0) (Rlt y0 d0) Hxy0).
We prove the intermediate claim HxyLeft3: ((x = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b0) ∧ Rlt c y0.
An exact proof term for the current goal is (andEL (((x = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b0) ∧ Rlt c y0) (Rlt y0 d0) Hxy0).
We prove the intermediate claim Hcy0: Rlt c y0.
An exact proof term for the current goal is (andER ((x = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b0) (Rlt c y0) HxyLeft3).
We prove the intermediate claim HxyLeft2: (x = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b0.
An exact proof term for the current goal is (andEL ((x = (x0,y0) ∧ Rlt a x0) ∧ Rlt x0 b0) (Rlt c y0) HxyLeft3).
We prove the intermediate claim Hx0b0: Rlt x0 b0.
An exact proof term for the current goal is (andER (x = (x0,y0) ∧ Rlt a x0) (Rlt x0 b0) HxyLeft2).
We prove the intermediate claim HxyLeft1: x = (x0,y0) ∧ Rlt a x0.
An exact proof term for the current goal is (andEL (x = (x0,y0) ∧ Rlt a x0) (Rlt x0 b0) HxyLeft2).
We prove the intermediate claim Hax0: Rlt a x0.
An exact proof term for the current goal is (andER (x = (x0,y0)) (Rlt a x0) HxyLeft1).
We prove the intermediate claim HxEq: x = (x0,y0).
An exact proof term for the current goal is (andEL (x = (x0,y0)) (Rlt a x0) HxyLeft1).
We prove the intermediate claim Hx0R: x0 ∈ R.
An exact proof term for the current goal is (RltE_right a x0 Hax0).
We prove the intermediate claim Hy0R: y0 ∈ R.
An exact proof term for the current goal is (RltE_right c y0 Hcy0).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0R).
We prove the intermediate claim Hy0S: SNo y0.
An exact proof term for the current goal is (real_SNo y0 Hy0R).
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 Hb0S: SNo b0.
An exact proof term for the current goal is (real_SNo b0 Hb0R).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcR).
We prove the intermediate claim Hd0S: SNo d0.
An exact proof term for the current goal is (real_SNo d0 Hd0R).
Set m1 to be the term add_SNo x0 (minus_SNo a).
Set m2 to be the term add_SNo b0 (minus_SNo x0).
Set m3 to be the term add_SNo y0 (minus_SNo c).
Set m4 to be the term add_SNo d0 (minus_SNo y0).
We prove the intermediate claim Hm1R: m1 ∈ R.
An exact proof term for the current goal is (real_add_SNo x0 Hx0R (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim Hm2R: m2 ∈ R.
An exact proof term for the current goal is (real_add_SNo b0 Hb0R (minus_SNo x0) (real_minus_SNo x0 Hx0R)).
We prove the intermediate claim Hm3R: m3 ∈ R.
An exact proof term for the current goal is (real_add_SNo y0 Hy0R (minus_SNo c) (real_minus_SNo c HcR)).
We prove the intermediate claim Hm4R: m4 ∈ R.
An exact proof term for the current goal is (real_add_SNo d0 Hd0R (minus_SNo y0) (real_minus_SNo y0 Hy0R)).
We prove the intermediate claim Hm1S: SNo m1.
An exact proof term for the current goal is (real_SNo m1 Hm1R).
We prove the intermediate claim Hm2S: SNo m2.
An exact proof term for the current goal is (real_SNo m2 Hm2R).
We prove the intermediate claim Hm3S: SNo m3.
An exact proof term for the current goal is (real_SNo m3 Hm3R).
We prove the intermediate claim Hm4S: SNo m4.
An exact proof term for the current goal is (real_SNo m4 Hm4R).
We prove the intermediate claim Hax0Slt: a < x0.
An exact proof term for the current goal is (RltE_lt a x0 Hax0).
We prove the intermediate claim Hx0b0Slt: x0 < b0.
An exact proof term for the current goal is (RltE_lt x0 b0 Hx0b0).
We prove the intermediate claim Hcy0Slt: c < y0.
An exact proof term for the current goal is (RltE_lt c y0 Hcy0).
We prove the intermediate claim Hy0d0Slt: y0 < d0.
An exact proof term for the current goal is (RltE_lt y0 d0 Hy0d0).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim Hmx0S: SNo (minus_SNo x0).
An exact proof term for the current goal is (SNo_minus_SNo x0 Hx0S).
We prove the intermediate claim HmcS: SNo (minus_SNo c).
An exact proof term for the current goal is (SNo_minus_SNo c HcS).
We prove the intermediate claim Hmy0S: SNo (minus_SNo y0).
An exact proof term for the current goal is (SNo_minus_SNo y0 Hy0S).
We prove the intermediate claim Hm1posS: 0 < m1.
We prove the intermediate claim Hlt: add_SNo (minus_SNo a) a < add_SNo (minus_SNo a) x0.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo a) a x0 HmaS HaS Hx0S Hax0Slt).
We prove the intermediate claim H0eq: add_SNo (minus_SNo a) a = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv a HaS).
We prove the intermediate claim Hm1eq: add_SNo (minus_SNo a) x0 = m1.
We prove the intermediate claim Hcom: add_SNo (minus_SNo a) x0 = add_SNo x0 (minus_SNo a).
An exact proof term for the current goal is (add_SNo_com (minus_SNo a) x0 HmaS Hx0S).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using H0eq (from right to left) at position 1.
rewrite the current goal using Hm1eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hm2posS: 0 < m2.
We prove the intermediate claim Hlt: add_SNo (minus_SNo x0) x0 < add_SNo (minus_SNo x0) b0.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo x0) x0 b0 Hmx0S Hx0S Hb0S Hx0b0Slt).
We prove the intermediate claim H0eq: add_SNo (minus_SNo x0) x0 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv x0 Hx0S).
We prove the intermediate claim Hm2eq: add_SNo (minus_SNo x0) b0 = m2.
We prove the intermediate claim Hcom: add_SNo (minus_SNo x0) b0 = add_SNo b0 (minus_SNo x0).
An exact proof term for the current goal is (add_SNo_com (minus_SNo x0) b0 Hmx0S Hb0S).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using H0eq (from right to left) at position 1.
rewrite the current goal using Hm2eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hm3posS: 0 < m3.
We prove the intermediate claim Hlt: add_SNo (minus_SNo c) c < add_SNo (minus_SNo c) y0.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo c) c y0 HmcS HcS Hy0S Hcy0Slt).
We prove the intermediate claim H0eq: add_SNo (minus_SNo c) c = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv c HcS).
We prove the intermediate claim Hm3eq: add_SNo (minus_SNo c) y0 = m3.
We prove the intermediate claim Hcom: add_SNo (minus_SNo c) y0 = add_SNo y0 (minus_SNo c).
An exact proof term for the current goal is (add_SNo_com (minus_SNo c) y0 HmcS Hy0S).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using H0eq (from right to left) at position 1.
rewrite the current goal using Hm3eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hm4posS: 0 < m4.
We prove the intermediate claim Hlt: add_SNo (minus_SNo y0) y0 < add_SNo (minus_SNo y0) d0.
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo y0) y0 d0 Hmy0S Hy0S Hd0S Hy0d0Slt).
We prove the intermediate claim H0eq: add_SNo (minus_SNo y0) y0 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv y0 Hy0S).
We prove the intermediate claim Hm4eq: add_SNo (minus_SNo y0) d0 = m4.
We prove the intermediate claim Hcom: add_SNo (minus_SNo y0) d0 = add_SNo d0 (minus_SNo y0).
An exact proof term for the current goal is (add_SNo_com (minus_SNo y0) d0 Hmy0S Hd0S).
rewrite the current goal using Hcom (from left to right).
Use reflexivity.
rewrite the current goal using H0eq (from right to left) at position 1.
rewrite the current goal using Hm4eq (from right to left) at position 1.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hm1pos: Rlt 0 m1.
An exact proof term for the current goal is (RltI 0 m1 real_0 Hm1R Hm1posS).
We prove the intermediate claim Hm2pos: Rlt 0 m2.
An exact proof term for the current goal is (RltI 0 m2 real_0 Hm2R Hm2posS).
We prove the intermediate claim Hm3pos: Rlt 0 m3.
An exact proof term for the current goal is (RltI 0 m3 real_0 Hm3R Hm3posS).
We prove the intermediate claim Hm4pos: Rlt 0 m4.
An exact proof term for the current goal is (RltI 0 m4 real_0 Hm4R Hm4posS).
We prove the intermediate claim Hexr3: ∃r3 : set, r3 ∈ R ∧ Rlt 0 r3 ∧ Rlt r3 m1 ∧ Rlt r3 m2 ∧ Rlt r3 m3 ∧ Rlt r3 m4.
An exact proof term for the current goal is (exists_eps_lt_four_pos_Euclid m1 m2 m3 m4 Hm1R Hm2R Hm3R Hm4R Hm1pos Hm2pos Hm3pos Hm4pos).
Apply Hexr3 to the current goal.
Let r3 be given.
Assume Hr3.
We prove the intermediate claim Hr3m4: Rlt r3 m4.
An exact proof term for the current goal is (andER ((((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2) ∧ Rlt r3 m3) (Rlt r3 m4) Hr3).
We prove the intermediate claim Hr3Left5: (((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2) ∧ Rlt r3 m3.
An exact proof term for the current goal is (andEL ((((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2) ∧ Rlt r3 m3) (Rlt r3 m4) Hr3).
We prove the intermediate claim Hr3m3: Rlt r3 m3.
An exact proof term for the current goal is (andER (((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2) (Rlt r3 m3) Hr3Left5).
We prove the intermediate claim Hr3Left4: ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2.
An exact proof term for the current goal is (andEL (((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) ∧ Rlt r3 m2) (Rlt r3 m3) Hr3Left5).
We prove the intermediate claim Hr3m2: Rlt r3 m2.
An exact proof term for the current goal is (andER ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) (Rlt r3 m2) Hr3Left4).
We prove the intermediate claim Hr3Left3: (r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1.
An exact proof term for the current goal is (andEL ((r3 ∈ R ∧ Rlt 0 r3) ∧ Rlt r3 m1) (Rlt r3 m2) Hr3Left4).
We prove the intermediate claim Hr3m1: Rlt r3 m1.
An exact proof term for the current goal is (andER (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 m1) Hr3Left3).
We prove the intermediate claim Hr3Pair: r3 ∈ R ∧ Rlt 0 r3.
An exact proof term for the current goal is (andEL (r3 ∈ R ∧ Rlt 0 r3) (Rlt r3 m1) Hr3Left3).
We prove the intermediate claim Hr3R: r3 ∈ R.
An exact proof term for the current goal is (andEL (r3 ∈ R) (Rlt 0 r3) Hr3Pair).
We prove the intermediate claim Hr3pos: Rlt 0 r3.
An exact proof term for the current goal is (andER (r3 ∈ R) (Rlt 0 r3) Hr3Pair).
We use r3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr3pos.
Let p be given.
Assume HpE: p ∈ EuclidPlane.
Assume Hdp: Rlt (distance_R2 p x) r3.
We will prove p ∈ b.
rewrite the current goal using HbEq (from left to right).
We will prove p ∈ Rect.
Set xp to be the term R2_xcoord p.
Set yp to be the term R2_ycoord p.
We prove the intermediate claim HxpDef: xp = R2_xcoord p.
Use reflexivity.
We prove the intermediate claim HypDef: yp = R2_ycoord p.
Use reflexivity.
We prove the intermediate claim HxpR: xp ∈ R.
rewrite the current goal using HxpDef (from left to right).
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R p HpE).
We prove the intermediate claim HypR: yp ∈ R.
rewrite the current goal using HypDef (from left to right).
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R p HpE).
We prove the intermediate claim HxpS: SNo xp.
An exact proof term for the current goal is (real_SNo xp HxpR).
We prove the intermediate claim HypS: SNo yp.
An exact proof term for the current goal is (real_SNo yp HypR).
We prove the intermediate claim Hxcoord: R2_xcoord x = x0.
We will prove R2_xcoord x = x0.
rewrite the current goal using HxEq (from left to right) at position 1.
An exact proof term for the current goal is (R2_xcoord_tuple x0 y0).
We prove the intermediate claim Hycoord: R2_ycoord x = y0.
We will prove R2_ycoord x = y0.
rewrite the current goal using HxEq (from left to right) at position 1.
An exact proof term for the current goal is (R2_ycoord_tuple x0 y0).
We prove the intermediate claim Hr3S: SNo r3.
An exact proof term for the current goal is (real_SNo r3 Hr3R).
We prove the intermediate claim Hr3posS: 0 < r3.
An exact proof term for the current goal is (RltE_lt 0 r3 Hr3pos).
We prove the intermediate claim Habsdx: abs_SNo (add_SNo xp (minus_SNo x0)) < r3.
We will prove abs_SNo (add_SNo xp (minus_SNo x0)) < r3.
rewrite the current goal using HxpDef (from left to right) at position 1.
rewrite the current goal using Hxcoord (from right to left) at position 1.
An exact proof term for the current goal is (abs_xcoord_lt_of_distance_lt p x r3 HpE HxE Hr3R Hdp).
We prove the intermediate claim Habsdy: abs_SNo (add_SNo yp (minus_SNo y0)) < r3.
We will prove abs_SNo (add_SNo yp (minus_SNo y0)) < r3.
rewrite the current goal using HypDef (from left to right) at position 1.
rewrite the current goal using Hycoord (from right to left) at position 1.
An exact proof term for the current goal is (abs_ycoord_lt_of_distance_lt p x r3 HpE HxE Hr3R Hdp).
Set dx to be the term add_SNo xp (minus_SNo x0).
Set dy to be the term add_SNo yp (minus_SNo y0).
We prove the intermediate claim HdxDef: dx = add_SNo xp (minus_SNo x0).
Use reflexivity.
We prove the intermediate claim HdyDef: dy = add_SNo yp (minus_SNo y0).
Use reflexivity.
We prove the intermediate claim HdxR: dx ∈ R.
rewrite the current goal using HdxDef (from left to right).
An exact proof term for the current goal is (real_add_SNo xp HxpR (minus_SNo x0) (real_minus_SNo x0 Hx0R)).
We prove the intermediate claim HdyR: dy ∈ R.
rewrite the current goal using HdyDef (from left to right).
An exact proof term for the current goal is (real_add_SNo yp HypR (minus_SNo y0) (real_minus_SNo y0 Hy0R)).
We prove the intermediate claim HdxS: SNo dx.
An exact proof term for the current goal is (real_SNo dx HdxR).
We prove the intermediate claim HdyS: SNo dy.
An exact proof term for the current goal is (real_SNo dy HdyR).
We prove the intermediate claim HdxLt: dx < r3.
rewrite the current goal using HdxDef (from left to right) at position 1.
An exact proof term for the current goal is (abs_SNo_lt_imp_lt (add_SNo xp (minus_SNo x0)) r3 (real_SNo (add_SNo xp (minus_SNo x0)) HdxR) Hr3S Hr3posS Habsdx).
We prove the intermediate claim HdyLt: dy < r3.
rewrite the current goal using HdyDef (from left to right) at position 1.
An exact proof term for the current goal is (abs_SNo_lt_imp_lt (add_SNo yp (minus_SNo y0)) r3 (real_SNo (add_SNo yp (minus_SNo y0)) HdyR) Hr3S Hr3posS Habsdy).
We prove the intermediate claim HnegdxLt: minus_SNo dx < r3.
rewrite the current goal using HdxDef (from left to right) at position 1.
An exact proof term for the current goal is (abs_SNo_lt_imp_neg_lt (add_SNo xp (minus_SNo x0)) r3 (real_SNo (add_SNo xp (minus_SNo x0)) HdxR) Hr3S Hr3posS Habsdx).
We prove the intermediate claim HnegdyLt: minus_SNo dy < r3.
rewrite the current goal using HdyDef (from left to right) at position 1.
An exact proof term for the current goal is (abs_SNo_lt_imp_neg_lt (add_SNo yp (minus_SNo y0)) r3 (real_SNo (add_SNo yp (minus_SNo y0)) HdyR) Hr3S Hr3posS Habsdy).
We prove the intermediate claim HnegdxEq: minus_SNo dx = add_SNo x0 (minus_SNo xp).
We will prove minus_SNo dx = add_SNo x0 (minus_SNo xp).
rewrite the current goal using HdxDef (from left to right) at position 1.
We prove the intermediate claim Hmx0S: SNo (minus_SNo x0).
An exact proof term for the current goal is (SNo_minus_SNo x0 Hx0S).
We prove the intermediate claim HmxpS: SNo (minus_SNo xp).
An exact proof term for the current goal is (SNo_minus_SNo xp HxpS).
We prove the intermediate claim Hneg: minus_SNo (add_SNo xp (minus_SNo x0)) = add_SNo (minus_SNo xp) (minus_SNo (minus_SNo x0)).
An exact proof term for the current goal is (minus_add_SNo_distr xp (minus_SNo x0) HxpS Hmx0S).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo x0) = x0.
An exact proof term for the current goal is (minus_SNo_invol x0 Hx0S).
We prove the intermediate claim Hneg2: minus_SNo (add_SNo xp (minus_SNo x0)) = add_SNo (minus_SNo xp) x0.
rewrite the current goal using Hinv (from right to left) at position 2.
An exact proof term for the current goal is Hneg.
We prove the intermediate claim Hcom: add_SNo (minus_SNo xp) x0 = add_SNo x0 (minus_SNo xp).
An exact proof term for the current goal is (add_SNo_com (minus_SNo xp) x0 HmxpS Hx0S).
rewrite the current goal using Hcom (from right to left).
An exact proof term for the current goal is Hneg2.
We prove the intermediate claim HnegdyEq: minus_SNo dy = add_SNo y0 (minus_SNo yp).
We will prove minus_SNo dy = add_SNo y0 (minus_SNo yp).
rewrite the current goal using HdyDef (from left to right) at position 1.
We prove the intermediate claim Hmy0S: SNo (minus_SNo y0).
An exact proof term for the current goal is (SNo_minus_SNo y0 Hy0S).
We prove the intermediate claim HmypS: SNo (minus_SNo yp).
An exact proof term for the current goal is (SNo_minus_SNo yp HypS).
We prove the intermediate claim Hneg: minus_SNo (add_SNo yp (minus_SNo y0)) = add_SNo (minus_SNo yp) (minus_SNo (minus_SNo y0)).
An exact proof term for the current goal is (minus_add_SNo_distr yp (minus_SNo y0) HypS Hmy0S).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo y0) = y0.
An exact proof term for the current goal is (minus_SNo_invol y0 Hy0S).
We prove the intermediate claim Hneg2: minus_SNo (add_SNo yp (minus_SNo y0)) = add_SNo (minus_SNo yp) y0.
rewrite the current goal using Hinv (from right to left) at position 2.
An exact proof term for the current goal is Hneg.
We prove the intermediate claim Hcom: add_SNo (minus_SNo yp) y0 = add_SNo y0 (minus_SNo yp).
An exact proof term for the current goal is (add_SNo_com (minus_SNo yp) y0 HmypS Hy0S).
rewrite the current goal using Hcom (from right to left).
An exact proof term for the current goal is Hneg2.
We prove the intermediate claim Hr3m1S: r3 < m1.
An exact proof term for the current goal is (RltE_lt r3 m1 Hr3m1).
We prove the intermediate claim Hr3m2S: r3 < m2.
An exact proof term for the current goal is (RltE_lt r3 m2 Hr3m2).
We prove the intermediate claim Hr3m3S: r3 < m3.
An exact proof term for the current goal is (RltE_lt r3 m3 Hr3m3).
We prove the intermediate claim Hr3m4S: r3 < m4.
An exact proof term for the current goal is (RltE_lt r3 m4 Hr3m4).
We prove the intermediate claim Hx0Lt_xpr3: x0 < add_SNo xp r3.
We will prove x0 < add_SNo xp r3.
We prove the intermediate claim Hx0mxpLt: add_SNo x0 (minus_SNo xp) < r3.
We will prove add_SNo x0 (minus_SNo xp) < r3.
rewrite the current goal using HnegdxEq (from right to left) at position 1.
An exact proof term for the current goal is HnegdxLt.
We prove the intermediate claim Hx0mxpS: SNo (add_SNo x0 (minus_SNo xp)).
An exact proof term for the current goal is (real_SNo (add_SNo x0 (minus_SNo xp)) (real_add_SNo x0 Hx0R (minus_SNo xp) (real_minus_SNo xp HxpR))).
We prove the intermediate claim Htmp: add_SNo xp (add_SNo x0 (minus_SNo xp)) < add_SNo xp r3.
An exact proof term for the current goal is (add_SNo_Lt2 xp (add_SNo x0 (minus_SNo xp)) r3 HxpS Hx0mxpS Hr3S Hx0mxpLt).
We prove the intermediate claim HlhsEq: add_SNo xp (add_SNo x0 (minus_SNo xp)) = x0.
We prove the intermediate claim HmxpS: SNo (minus_SNo xp).
An exact proof term for the current goal is (SNo_minus_SNo xp HxpS).
We prove the intermediate claim Hassoc1: add_SNo xp (add_SNo x0 (minus_SNo xp)) = add_SNo (add_SNo xp x0) (minus_SNo xp).
An exact proof term for the current goal is (add_SNo_assoc xp x0 (minus_SNo xp) HxpS Hx0S HmxpS).
We prove the intermediate claim Hcom1: add_SNo xp x0 = add_SNo x0 xp.
An exact proof term for the current goal is (add_SNo_com xp x0 HxpS Hx0S).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo x0 xp) (minus_SNo xp) = add_SNo x0 (add_SNo xp (minus_SNo xp)).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc x0 xp (minus_SNo xp) Hx0S HxpS HmxpS).
We prove the intermediate claim Hinv: add_SNo xp (minus_SNo xp) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv xp HxpS).
We prove the intermediate claim Hz: add_SNo x0 0 = x0.
An exact proof term for the current goal is (add_SNo_0R x0 Hx0S).
We will prove add_SNo xp (add_SNo x0 (minus_SNo xp)) = x0.
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is Hz.
rewrite the current goal using HlhsEq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HxpLt_x0r3: xp < add_SNo x0 r3.
We will prove xp < add_SNo x0 r3.
We prove the intermediate claim HdxSlt: add_SNo xp (minus_SNo x0) < r3.
rewrite the current goal using HdxDef (from right to left) at position 1.
An exact proof term for the current goal is HdxLt.
We prove the intermediate claim HdxtermS: SNo (add_SNo xp (minus_SNo x0)).
An exact proof term for the current goal is (real_SNo (add_SNo xp (minus_SNo x0)) HdxR).
We prove the intermediate claim Htmp: add_SNo x0 (add_SNo xp (minus_SNo x0)) < add_SNo x0 r3.
An exact proof term for the current goal is (add_SNo_Lt2 x0 (add_SNo xp (minus_SNo x0)) r3 Hx0S HdxtermS Hr3S HdxSlt).
We prove the intermediate claim HlhsEq: add_SNo x0 (add_SNo xp (minus_SNo x0)) = xp.
We prove the intermediate claim Hmx0S: SNo (minus_SNo x0).
An exact proof term for the current goal is (SNo_minus_SNo x0 Hx0S).
We prove the intermediate claim Hassoc1: add_SNo x0 (add_SNo xp (minus_SNo x0)) = add_SNo (add_SNo x0 xp) (minus_SNo x0).
An exact proof term for the current goal is (add_SNo_assoc x0 xp (minus_SNo x0) Hx0S HxpS Hmx0S).
We prove the intermediate claim Hcom1: add_SNo x0 xp = add_SNo xp x0.
An exact proof term for the current goal is (add_SNo_com x0 xp Hx0S HxpS).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo xp x0) (minus_SNo x0) = add_SNo xp (add_SNo x0 (minus_SNo x0)).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc xp x0 (minus_SNo x0) HxpS Hx0S Hmx0S).
We prove the intermediate claim Hinv: add_SNo x0 (minus_SNo x0) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv x0 Hx0S).
We prove the intermediate claim Hz: add_SNo xp 0 = xp.
An exact proof term for the current goal is (add_SNo_0R xp HxpS).
We will prove add_SNo x0 (add_SNo xp (minus_SNo x0)) = xp.
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is Hz.
rewrite the current goal using HlhsEq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hx0r3Lt_b0: add_SNo x0 r3 < b0.
We will prove add_SNo x0 r3 < b0.
We prove the intermediate claim Htmp: add_SNo x0 r3 < add_SNo x0 m2.
An exact proof term for the current goal is (add_SNo_Lt2 x0 r3 m2 Hx0S Hr3S Hm2S Hr3m2S).
We prove the intermediate claim HrhsEq: add_SNo x0 m2 = b0.
We will prove add_SNo x0 m2 = b0.
rewrite the current goal using (add_SNo_com x0 m2 Hx0S Hm2S) (from left to right).
rewrite the current goal using (add_SNo_assoc b0 (minus_SNo x0) x0 Hb0S Hmx0S Hx0S) (from right to left) at position 1.
We prove the intermediate claim Hinv: add_SNo (minus_SNo x0) x0 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv x0 Hx0S).
rewrite the current goal using Hinv (from left to right) at position 1.
An exact proof term for the current goal is (add_SNo_0R b0 Hb0S).
We will prove add_SNo x0 r3 < b0.
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hm1Def: m1 = add_SNo x0 (minus_SNo a).
Use reflexivity.
We prove the intermediate claim Hr3m1Lt: r3 < m1.
An exact proof term for the current goal is Hr3m1S.
We prove the intermediate claim Har3Lt_am1: add_SNo a r3 < add_SNo a m1.
An exact proof term for the current goal is (add_SNo_Lt2 a r3 m1 HaS Hr3S Hm1S Hr3m1Lt).
We prove the intermediate claim Ham1Eq: add_SNo a m1 = x0.
We will prove add_SNo a m1 = x0.
rewrite the current goal using Hm1Def (from left to right).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim Hassoc1: add_SNo a (add_SNo x0 (minus_SNo a)) = add_SNo (add_SNo a x0) (minus_SNo a).
An exact proof term for the current goal is (add_SNo_assoc a x0 (minus_SNo a) HaS Hx0S HmaS).
We prove the intermediate claim Hcom1: add_SNo a x0 = add_SNo x0 a.
An exact proof term for the current goal is (add_SNo_com a x0 HaS Hx0S).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo x0 a) (minus_SNo a) = add_SNo x0 (add_SNo a (minus_SNo a)).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc x0 a (minus_SNo a) Hx0S HaS HmaS).
We prove the intermediate claim Hinv: add_SNo a (minus_SNo a) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv a HaS).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R x0 Hx0S).
We prove the intermediate claim Har3Lt_x0: add_SNo a r3 < x0.
We will prove add_SNo a r3 < x0.
rewrite the current goal using Ham1Eq (from right to left).
An exact proof term for the current goal is Har3Lt_am1.
We prove the intermediate claim Har3S: SNo (add_SNo a r3).
An exact proof term for the current goal is (real_SNo (add_SNo a r3) (real_add_SNo a HaR r3 Hr3R)).
We prove the intermediate claim Hx0Lt_xpr3S: x0 < add_SNo xp r3.
An exact proof term for the current goal is Hx0Lt_xpr3.
We prove the intermediate claim Hxpr3S: SNo (add_SNo xp r3).
An exact proof term for the current goal is (real_SNo (add_SNo xp r3) (real_add_SNo xp HxpR r3 Hr3R)).
We prove the intermediate claim Har3Lt_xpr3: add_SNo a r3 < add_SNo xp r3.
An exact proof term for the current goal is (SNoLt_tra (add_SNo a r3) x0 (add_SNo xp r3) Har3S Hx0S Hxpr3S Har3Lt_x0 Hx0Lt_xpr3S).
We prove the intermediate claim Hmr3S: SNo (minus_SNo r3).
An exact proof term for the current goal is (SNo_minus_SNo r3 Hr3S).
We prove the intermediate claim HcancelL: add_SNo (minus_SNo r3) (add_SNo a r3) = a.
We prove the intermediate claim Hassoc1: add_SNo (minus_SNo r3) (add_SNo a r3) = add_SNo (add_SNo (minus_SNo r3) a) r3.
An exact proof term for the current goal is (add_SNo_assoc (minus_SNo r3) a r3 Hmr3S HaS Hr3S).
We prove the intermediate claim Hcom1: add_SNo (minus_SNo r3) a = add_SNo a (minus_SNo r3).
An exact proof term for the current goal is (add_SNo_com (minus_SNo r3) a Hmr3S HaS).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo a (minus_SNo r3)) r3 = add_SNo a (add_SNo (minus_SNo r3) r3).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc a (minus_SNo r3) r3 HaS Hmr3S Hr3S).
We prove the intermediate claim Hinv: add_SNo (minus_SNo r3) r3 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv r3 Hr3S).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R a HaS).
We prove the intermediate claim HcancelR: add_SNo (minus_SNo r3) (add_SNo xp r3) = xp.
We prove the intermediate claim Hassoc1: add_SNo (minus_SNo r3) (add_SNo xp r3) = add_SNo (add_SNo (minus_SNo r3) xp) r3.
An exact proof term for the current goal is (add_SNo_assoc (minus_SNo r3) xp r3 Hmr3S HxpS Hr3S).
We prove the intermediate claim Hcom1: add_SNo (minus_SNo r3) xp = add_SNo xp (minus_SNo r3).
An exact proof term for the current goal is (add_SNo_com (minus_SNo r3) xp Hmr3S HxpS).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo xp (minus_SNo r3)) r3 = add_SNo xp (add_SNo (minus_SNo r3) r3).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc xp (minus_SNo r3) r3 HxpS Hmr3S Hr3S).
We prove the intermediate claim Hinv: add_SNo (minus_SNo r3) r3 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv r3 Hr3S).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R xp HxpS).
We prove the intermediate claim HtmpAx: add_SNo (minus_SNo r3) (add_SNo a r3) < add_SNo (minus_SNo r3) (add_SNo xp r3).
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo r3) (add_SNo a r3) (add_SNo xp r3) Hmr3S Har3S Hxpr3S Har3Lt_xpr3).
We prove the intermediate claim HaxSlt: a < xp.
We will prove a < xp.
rewrite the current goal using HcancelL (from right to left) at position 1.
rewrite the current goal using HcancelR (from right to left).
An exact proof term for the current goal is HtmpAx.
We prove the intermediate claim HaxRlt: Rlt a xp.
An exact proof term for the current goal is (RltI a xp HaR HxpR HaxSlt).
We prove the intermediate claim Hx0r3S: SNo (add_SNo x0 r3).
An exact proof term for the current goal is (real_SNo (add_SNo x0 r3) (real_add_SNo x0 Hx0R r3 Hr3R)).
We prove the intermediate claim HxpLt_b0S: xp < b0.
An exact proof term for the current goal is (SNoLt_tra xp (add_SNo x0 r3) b0 HxpS Hx0r3S Hb0S HxpLt_x0r3 Hx0r3Lt_b0).
We prove the intermediate claim HxpLt_b0: Rlt xp b0.
An exact proof term for the current goal is (RltI xp b0 HxpR Hb0R HxpLt_b0S).
We prove the intermediate claim Hy0Lt_ypr3: y0 < add_SNo yp r3.
We will prove y0 < add_SNo yp r3.
We prove the intermediate claim Hy0mypLt: add_SNo y0 (minus_SNo yp) < r3.
We will prove add_SNo y0 (minus_SNo yp) < r3.
rewrite the current goal using HnegdyEq (from right to left) at position 1.
An exact proof term for the current goal is HnegdyLt.
We prove the intermediate claim Hy0mypS: SNo (add_SNo y0 (minus_SNo yp)).
An exact proof term for the current goal is (real_SNo (add_SNo y0 (minus_SNo yp)) (real_add_SNo y0 Hy0R (minus_SNo yp) (real_minus_SNo yp HypR))).
We prove the intermediate claim Htmp: add_SNo yp (add_SNo y0 (minus_SNo yp)) < add_SNo yp r3.
An exact proof term for the current goal is (add_SNo_Lt2 yp (add_SNo y0 (minus_SNo yp)) r3 HypS Hy0mypS Hr3S Hy0mypLt).
We prove the intermediate claim HlhsEq: add_SNo yp (add_SNo y0 (minus_SNo yp)) = y0.
We prove the intermediate claim HmypS: SNo (minus_SNo yp).
An exact proof term for the current goal is (SNo_minus_SNo yp HypS).
We prove the intermediate claim Hassoc1: add_SNo yp (add_SNo y0 (minus_SNo yp)) = add_SNo (add_SNo yp y0) (minus_SNo yp).
An exact proof term for the current goal is (add_SNo_assoc yp y0 (minus_SNo yp) HypS Hy0S HmypS).
We prove the intermediate claim Hcom1: add_SNo yp y0 = add_SNo y0 yp.
An exact proof term for the current goal is (add_SNo_com yp y0 HypS Hy0S).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo y0 yp) (minus_SNo yp) = add_SNo y0 (add_SNo yp (minus_SNo yp)).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc y0 yp (minus_SNo yp) Hy0S HypS HmypS).
We prove the intermediate claim Hinv: add_SNo yp (minus_SNo yp) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv yp HypS).
We will prove add_SNo yp (add_SNo y0 (minus_SNo yp)) = y0.
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R y0 Hy0S).
rewrite the current goal using HlhsEq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim HypLt_y0r3: yp < add_SNo y0 r3.
We will prove yp < add_SNo y0 r3.
We prove the intermediate claim Hypmy0Lt: add_SNo yp (minus_SNo y0) < r3.
We will prove add_SNo yp (minus_SNo y0) < r3.
rewrite the current goal using HdyDef (from right to left) at position 1.
An exact proof term for the current goal is HdyLt.
We prove the intermediate claim Hypmy0S: SNo (add_SNo yp (minus_SNo y0)).
An exact proof term for the current goal is (real_SNo (add_SNo yp (minus_SNo y0)) (real_add_SNo yp HypR (minus_SNo y0) (real_minus_SNo y0 Hy0R))).
We prove the intermediate claim Htmp: add_SNo y0 (add_SNo yp (minus_SNo y0)) < add_SNo y0 r3.
An exact proof term for the current goal is (add_SNo_Lt2 y0 (add_SNo yp (minus_SNo y0)) r3 Hy0S Hypmy0S Hr3S Hypmy0Lt).
We prove the intermediate claim HlhsEq: add_SNo y0 (add_SNo yp (minus_SNo y0)) = yp.
We prove the intermediate claim Hmy0S: SNo (minus_SNo y0).
An exact proof term for the current goal is (SNo_minus_SNo y0 Hy0S).
We prove the intermediate claim Hassoc1: add_SNo y0 (add_SNo yp (minus_SNo y0)) = add_SNo (add_SNo y0 yp) (minus_SNo y0).
An exact proof term for the current goal is (add_SNo_assoc y0 yp (minus_SNo y0) Hy0S HypS Hmy0S).
We prove the intermediate claim Hcom1: add_SNo y0 yp = add_SNo yp y0.
An exact proof term for the current goal is (add_SNo_com y0 yp Hy0S HypS).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo yp y0) (minus_SNo y0) = add_SNo yp (add_SNo y0 (minus_SNo y0)).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc yp y0 (minus_SNo y0) HypS Hy0S Hmy0S).
We prove the intermediate claim Hinv: add_SNo y0 (minus_SNo y0) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv y0 Hy0S).
We will prove add_SNo y0 (add_SNo yp (minus_SNo y0)) = yp.
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R yp HypS).
rewrite the current goal using HlhsEq (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hy0r3Lt_d0: add_SNo y0 r3 < d0.
We will prove add_SNo y0 r3 < d0.
We prove the intermediate claim Htmp: add_SNo y0 r3 < add_SNo y0 m4.
An exact proof term for the current goal is (add_SNo_Lt2 y0 r3 m4 Hy0S Hr3S Hm4S Hr3m4S).
We prove the intermediate claim HrhsEq: add_SNo y0 m4 = d0.
We will prove add_SNo y0 m4 = d0.
We prove the intermediate claim Hmy0S: SNo (minus_SNo y0).
An exact proof term for the current goal is (SNo_minus_SNo y0 Hy0S).
rewrite the current goal using (add_SNo_com y0 m4 Hy0S Hm4S) (from left to right).
rewrite the current goal using (add_SNo_assoc d0 (minus_SNo y0) y0 Hd0S Hmy0S Hy0S) (from right to left) at position 1.
We prove the intermediate claim Hinv: add_SNo (minus_SNo y0) y0 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv y0 Hy0S).
rewrite the current goal using Hinv (from left to right) at position 1.
An exact proof term for the current goal is (add_SNo_0R d0 Hd0S).
We will prove add_SNo y0 r3 < d0.
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hy0r3S: SNo (add_SNo y0 r3).
An exact proof term for the current goal is (real_SNo (add_SNo y0 r3) (real_add_SNo y0 Hy0R r3 Hr3R)).
We prove the intermediate claim HypLt_d0S: yp < d0.
An exact proof term for the current goal is (SNoLt_tra yp (add_SNo y0 r3) d0 HypS Hy0r3S Hd0S HypLt_y0r3 Hy0r3Lt_d0).
We prove the intermediate claim HypLt_d0: Rlt yp d0.
An exact proof term for the current goal is (RltI yp d0 HypR Hd0R HypLt_d0S).
We prove the intermediate claim Hr3m3Lt: r3 < m3.
An exact proof term for the current goal is Hr3m3S.
We prove the intermediate claim Hcr3Lt_cm3: add_SNo c r3 < add_SNo c m3.
An exact proof term for the current goal is (add_SNo_Lt2 c r3 m3 HcS Hr3S Hm3S Hr3m3Lt).
We prove the intermediate claim Hcm3Eq: add_SNo c m3 = y0.
We will prove add_SNo c m3 = y0.
We prove the intermediate claim HmcS: SNo (minus_SNo c).
An exact proof term for the current goal is (SNo_minus_SNo c HcS).
We prove the intermediate claim Hassoc1: add_SNo c (add_SNo y0 (minus_SNo c)) = add_SNo (add_SNo c y0) (minus_SNo c).
An exact proof term for the current goal is (add_SNo_assoc c y0 (minus_SNo c) HcS Hy0S HmcS).
We prove the intermediate claim Hcom1: add_SNo c y0 = add_SNo y0 c.
An exact proof term for the current goal is (add_SNo_com c y0 HcS Hy0S).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo y0 c) (minus_SNo c) = add_SNo y0 (add_SNo c (minus_SNo c)).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc y0 c (minus_SNo c) Hy0S HcS HmcS).
We prove the intermediate claim Hinv: add_SNo c (minus_SNo c) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv c HcS).
We will prove add_SNo c m3 = y0.
We prove the intermediate claim Hm3Def: m3 = add_SNo y0 (minus_SNo c).
Use reflexivity.
rewrite the current goal using Hm3Def (from left to right).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R y0 Hy0S).
We prove the intermediate claim Hcr3Lt_y0: add_SNo c r3 < y0.
We will prove add_SNo c r3 < y0.
rewrite the current goal using Hcm3Eq (from right to left).
An exact proof term for the current goal is Hcr3Lt_cm3.
We prove the intermediate claim Hcr3S: SNo (add_SNo c r3).
An exact proof term for the current goal is (real_SNo (add_SNo c r3) (real_add_SNo c HcR r3 Hr3R)).
We prove the intermediate claim Hypr3S: SNo (add_SNo yp r3).
An exact proof term for the current goal is (real_SNo (add_SNo yp r3) (real_add_SNo yp HypR r3 Hr3R)).
We prove the intermediate claim Hcr3Lt_ypr3: add_SNo c r3 < add_SNo yp r3.
An exact proof term for the current goal is (SNoLt_tra (add_SNo c r3) y0 (add_SNo yp r3) Hcr3S Hy0S Hypr3S Hcr3Lt_y0 Hy0Lt_ypr3).
We prove the intermediate claim HcancelLc: add_SNo (minus_SNo r3) (add_SNo c r3) = c.
We prove the intermediate claim Hassoc1: add_SNo (minus_SNo r3) (add_SNo c r3) = add_SNo (add_SNo (minus_SNo r3) c) r3.
An exact proof term for the current goal is (add_SNo_assoc (minus_SNo r3) c r3 Hmr3S HcS Hr3S).
We prove the intermediate claim Hcom1: add_SNo (minus_SNo r3) c = add_SNo c (minus_SNo r3).
An exact proof term for the current goal is (add_SNo_com (minus_SNo r3) c Hmr3S HcS).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo c (minus_SNo r3)) r3 = add_SNo c (add_SNo (minus_SNo r3) r3).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc c (minus_SNo r3) r3 HcS Hmr3S Hr3S).
We prove the intermediate claim Hinv: add_SNo (minus_SNo r3) r3 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv r3 Hr3S).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R c HcS).
We prove the intermediate claim HcancelRyp: add_SNo (minus_SNo r3) (add_SNo yp r3) = yp.
We prove the intermediate claim Hassoc1: add_SNo (minus_SNo r3) (add_SNo yp r3) = add_SNo (add_SNo (minus_SNo r3) yp) r3.
An exact proof term for the current goal is (add_SNo_assoc (minus_SNo r3) yp r3 Hmr3S HypS Hr3S).
We prove the intermediate claim Hcom1: add_SNo (minus_SNo r3) yp = add_SNo yp (minus_SNo r3).
An exact proof term for the current goal is (add_SNo_com (minus_SNo r3) yp Hmr3S HypS).
We prove the intermediate claim Hassoc2: add_SNo (add_SNo yp (minus_SNo r3)) r3 = add_SNo yp (add_SNo (minus_SNo r3) r3).
Use symmetry.
An exact proof term for the current goal is (add_SNo_assoc yp (minus_SNo r3) r3 HypS Hmr3S Hr3S).
We prove the intermediate claim Hinv: add_SNo (minus_SNo r3) r3 = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_linv r3 Hr3S).
rewrite the current goal using Hassoc1 (from left to right).
rewrite the current goal using Hcom1 (from left to right).
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right).
An exact proof term for the current goal is (add_SNo_0R yp HypS).
We prove the intermediate claim HtmpCy: add_SNo (minus_SNo r3) (add_SNo c r3) < add_SNo (minus_SNo r3) (add_SNo yp r3).
An exact proof term for the current goal is (add_SNo_Lt2 (minus_SNo r3) (add_SNo c r3) (add_SNo yp r3) Hmr3S Hcr3S Hypr3S Hcr3Lt_ypr3).
We prove the intermediate claim HcySlt: c < yp.
We will prove c < yp.
rewrite the current goal using HcancelLc (from right to left) at position 1.
rewrite the current goal using HcancelRyp (from right to left).
An exact proof term for the current goal is HtmpCy.
We prove the intermediate claim HcyRlt: Rlt c yp.
An exact proof term for the current goal is (RltI c yp HcR HypR HcySlt).
We prove the intermediate claim HpEq: p = (xp,yp).
We will prove p = (xp,yp).
We prove the intermediate claim Heta: (R2_xcoord p,R2_ycoord p) = p.
An exact proof term for the current goal is (EuclidPlane_eta p HpE).
We prove the intermediate claim HxpEq: R2_xcoord p = xp.
Use symmetry.
An exact proof term for the current goal is HxpDef.
We prove the intermediate claim HypEq: R2_ycoord p = yp.
Use symmetry.
An exact proof term for the current goal is HypDef.
Use symmetry.
rewrite the current goal using HxpEq (from left to right) at position 1.
rewrite the current goal using HypEq (from left to right) at position 1.
An exact proof term for the current goal is Heta.
We prove the intermediate claim HpProp: ∃x1 y1 : set, p = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b0 ∧ Rlt c y1 ∧ Rlt y1 d0.
We use xp to witness the existential quantifier.
We use yp to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is HpEq.
An exact proof term for the current goal is HaxRlt.
An exact proof term for the current goal is HxpLt_b0.
An exact proof term for the current goal is HcyRlt.
An exact proof term for the current goal is HypLt_d0.
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ ∃x1 y1 : set, p0 = (x1,y1) ∧ Rlt a x1 ∧ Rlt x1 b0 ∧ Rlt c y1 ∧ Rlt y1 d0) p HpE HpProp).
∎