Let x, y and z be given.
Assume Hx: x ∈ EuclidPlane.
Assume Hy: y ∈ EuclidPlane.
Assume Hz: z ∈ EuclidPlane.
Set dxy to be the term distance_R2 x y.
Set dyz to be the term distance_R2 y z.
Set dxz to be the term distance_R2 x z.
Set s to be the term add_SNo dxy dyz.
Set dx_xy to be the term add_SNo (R2_xcoord x) (minus_SNo (R2_xcoord y)).
Set dy_xy to be the term add_SNo (R2_ycoord x) (minus_SNo (R2_ycoord y)).
Set dx_yz to be the term add_SNo (R2_xcoord y) (minus_SNo (R2_xcoord z)).
Set dy_yz to be the term add_SNo (R2_ycoord y) (minus_SNo (R2_ycoord z)).
Set dx_xz to be the term add_SNo (R2_xcoord x) (minus_SNo (R2_xcoord z)).
Set dy_xz to be the term add_SNo (R2_ycoord x) (minus_SNo (R2_ycoord z)).
We prove the intermediate claim HdxyR: dxy ∈ R.
An exact proof term for the current goal is (distance_R2_in_R x y Hx Hy).
We prove the intermediate claim HdyzR: dyz ∈ R.
An exact proof term for the current goal is (distance_R2_in_R y z Hy Hz).
We prove the intermediate claim HdxzR: dxz ∈ R.
An exact proof term for the current goal is (distance_R2_in_R x z Hx Hz).
We prove the intermediate claim HdxyS: SNo dxy.
An exact proof term for the current goal is (real_SNo dxy HdxyR).
We prove the intermediate claim HdyzS: SNo dyz.
An exact proof term for the current goal is (real_SNo dyz HdyzR).
We prove the intermediate claim HdxzS: SNo dxz.
An exact proof term for the current goal is (real_SNo dxz HdxzR).
We prove the intermediate claim H0ledxy: 0 ≤ dxy.
An exact proof term for the current goal is (distance_R2_nonneg x y Hx Hy).
We prove the intermediate claim H0ledyz: 0 ≤ dyz.
An exact proof term for the current goal is (distance_R2_nonneg y z Hy Hz).
We prove the intermediate claim H0ledxz: 0 ≤ dxz.
An exact proof term for the current goal is (distance_R2_nonneg x z Hx Hz).
We prove the intermediate claim Hx0R: R2_xcoord x ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R x Hx).
We prove the intermediate claim Hx1R: R2_ycoord x ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R x Hx).
We prove the intermediate claim Hy0R: R2_xcoord y ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R y Hy).
We prove the intermediate claim Hy1R: R2_ycoord y ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R y Hy).
We prove the intermediate claim Hz0R: R2_xcoord z ∈ R.
An exact proof term for the current goal is (EuclidPlane_xcoord_in_R z Hz).
We prove the intermediate claim Hz1R: R2_ycoord z ∈ R.
An exact proof term for the current goal is (EuclidPlane_ycoord_in_R z Hz).
We prove the intermediate claim Hdx_xyR: dx_xy ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_xcoord x) Hx0R (minus_SNo (R2_xcoord y)) (real_minus_SNo (R2_xcoord y) Hy0R)).
We prove the intermediate claim Hdy_xyR: dy_xy ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_ycoord x) Hx1R (minus_SNo (R2_ycoord y)) (real_minus_SNo (R2_ycoord y) Hy1R)).
We prove the intermediate claim Hdx_yzR: dx_yz ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_xcoord y) Hy0R (minus_SNo (R2_xcoord z)) (real_minus_SNo (R2_xcoord z) Hz0R)).
We prove the intermediate claim Hdy_yzR: dy_yz ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_ycoord y) Hy1R (minus_SNo (R2_ycoord z)) (real_minus_SNo (R2_ycoord z) Hz1R)).
We prove the intermediate claim Hdx_xzR: dx_xz ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_xcoord x) Hx0R (minus_SNo (R2_xcoord z)) (real_minus_SNo (R2_xcoord z) Hz0R)).
We prove the intermediate claim Hdy_xzR: dy_xz ∈ R.
An exact proof term for the current goal is (real_add_SNo (R2_ycoord x) Hx1R (minus_SNo (R2_ycoord z)) (real_minus_SNo (R2_ycoord z) Hz1R)).
We prove the intermediate claim Hdx_xyS: SNo dx_xy.
An exact proof term for the current goal is (real_SNo dx_xy Hdx_xyR).
We prove the intermediate claim Hdy_xyS: SNo dy_xy.
An exact proof term for the current goal is (real_SNo dy_xy Hdy_xyR).
We prove the intermediate claim Hdx_yzS: SNo dx_yz.
An exact proof term for the current goal is (real_SNo dx_yz Hdx_yzR).
We prove the intermediate claim Hdy_yzS: SNo dy_yz.
An exact proof term for the current goal is (real_SNo dy_yz Hdy_yzR).
We prove the intermediate claim Hdx_xzS: SNo dx_xz.
An exact proof term for the current goal is (real_SNo dx_xz Hdx_xzR).
We prove the intermediate claim Hdy_xzS: SNo dy_xz.
An exact proof term for the current goal is (real_SNo dy_xz Hdy_xzR).
We prove the intermediate claim Hdx_decomp: dx_xz = add_SNo dx_xy dx_yz.
We will prove dx_xz = add_SNo dx_xy dx_yz.
We prove the intermediate claim Hx0S: SNo (R2_xcoord x).
An exact proof term for the current goal is (real_SNo (R2_xcoord x) Hx0R).
We prove the intermediate claim Hy0S: SNo (R2_xcoord y).
An exact proof term for the current goal is (real_SNo (R2_xcoord y) Hy0R).
We prove the intermediate claim Hz0S: SNo (R2_xcoord z).
An exact proof term for the current goal is (real_SNo (R2_xcoord z) Hz0R).
We prove the intermediate claim Hmy0S: SNo (minus_SNo (R2_xcoord y)).
An exact proof term for the current goal is (SNo_minus_SNo (R2_xcoord y) Hy0S).
We prove the intermediate claim Hmz0S: SNo (minus_SNo (R2_xcoord z)).
An exact proof term for the current goal is (SNo_minus_SNo (R2_xcoord z) Hz0S).
We prove the intermediate claim Hdx_xy_def: dx_xy = add_SNo (R2_xcoord x) (minus_SNo (R2_xcoord y)).
Use reflexivity.
We prove the intermediate claim Hdx_yz_def: dx_yz = add_SNo (R2_xcoord y) (minus_SNo (R2_xcoord z)).
Use reflexivity.
We prove the intermediate claim Hdx_xz_def: dx_xz = add_SNo (R2_xcoord x) (minus_SNo (R2_xcoord z)).
Use reflexivity.
rewrite the current goal using Hdx_xz_def (from left to right).
rewrite the current goal using Hdx_xy_def (from left to right).
rewrite the current goal using Hdx_yz_def (from left to right).
rewrite the current goal using (add_SNo_assoc (R2_xcoord x) (minus_SNo (R2_xcoord y)) (add_SNo (R2_xcoord y) (minus_SNo (R2_xcoord z))) Hx0S Hmy0S (SNo_add_SNo (R2_xcoord y) (minus_SNo (R2_xcoord z)) Hy0S Hmz0S)) (from right to left).
rewrite the current goal using (add_SNo_assoc (minus_SNo (R2_xcoord y)) (R2_xcoord y) (minus_SNo (R2_xcoord z)) Hmy0S Hy0S Hmz0S) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_linv (R2_xcoord y) Hy0S) (from left to right).
rewrite the current goal using (add_SNo_0L (minus_SNo (R2_xcoord z)) Hmz0S) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdy_decomp: dy_xz = add_SNo dy_xy dy_yz.
We will prove dy_xz = add_SNo dy_xy dy_yz.
We prove the intermediate claim Hx1S: SNo (R2_ycoord x).
An exact proof term for the current goal is (real_SNo (R2_ycoord x) Hx1R).
We prove the intermediate claim Hy1S: SNo (R2_ycoord y).
An exact proof term for the current goal is (real_SNo (R2_ycoord y) Hy1R).
We prove the intermediate claim Hz1S: SNo (R2_ycoord z).
An exact proof term for the current goal is (real_SNo (R2_ycoord z) Hz1R).
We prove the intermediate claim Hmy1S: SNo (minus_SNo (R2_ycoord y)).
An exact proof term for the current goal is (SNo_minus_SNo (R2_ycoord y) Hy1S).
We prove the intermediate claim Hmz1S: SNo (minus_SNo (R2_ycoord z)).
An exact proof term for the current goal is (SNo_minus_SNo (R2_ycoord z) Hz1S).
We prove the intermediate claim Hdy_xy_def: dy_xy = add_SNo (R2_ycoord x) (minus_SNo (R2_ycoord y)).
Use reflexivity.
We prove the intermediate claim Hdy_yz_def: dy_yz = add_SNo (R2_ycoord y) (minus_SNo (R2_ycoord z)).
Use reflexivity.
We prove the intermediate claim Hdy_xz_def: dy_xz = add_SNo (R2_ycoord x) (minus_SNo (R2_ycoord z)).
Use reflexivity.
rewrite the current goal using Hdy_xz_def (from left to right).
rewrite the current goal using Hdy_xy_def (from left to right).
rewrite the current goal using Hdy_yz_def (from left to right).
rewrite the current goal using (add_SNo_assoc (R2_ycoord x) (minus_SNo (R2_ycoord y)) (add_SNo (R2_ycoord y) (minus_SNo (R2_ycoord z))) Hx1S Hmy1S (SNo_add_SNo (R2_ycoord y) (minus_SNo (R2_ycoord z)) Hy1S Hmz1S)) (from right to left).
rewrite the current goal using (add_SNo_assoc (minus_SNo (R2_ycoord y)) (R2_ycoord y) (minus_SNo (R2_ycoord z)) Hmy1S Hy1S Hmz1S) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_linv (R2_ycoord y) Hy1S) (from left to right).
rewrite the current goal using (add_SNo_0L (minus_SNo (R2_ycoord z)) Hmz1S) (from left to right).
Use reflexivity.
rewrite the current goal using (distance_R2_sqr x z Hx Hz) (from left to right).
rewrite the current goal using Hdx_decomp (from left to right).
rewrite the current goal using Hdy_decomp (from left to right).
Set dx2_xy to be the term mul_SNo dx_xy dx_xy.
Set dy2_xy to be the term mul_SNo dy_xy dy_xy.
Set dx2_yz to be the term mul_SNo dx_yz dx_yz.
Set dy2_yz to be the term mul_SNo dy_yz dy_yz.
Set A to be the term add_SNo dx2_xy dy2_xy.
Set B to be the term add_SNo dx2_yz dy2_yz.
Set dot to be the term add_SNo (mul_SNo dx_xy dx_yz) (mul_SNo dy_xy dy_yz).
Set prod to be the term mul_SNo dxy dyz.
We prove the intermediate claim Hdx2xyS: SNo dx2_xy.
An exact proof term for the current goal is (SNo_mul_SNo dx_xy dx_xy Hdx_xyS Hdx_xyS).
We prove the intermediate claim Hdy2xyS: SNo dy2_xy.
An exact proof term for the current goal is (SNo_mul_SNo dy_xy dy_xy Hdy_xyS Hdy_xyS).
We prove the intermediate claim Hdx2yzS: SNo dx2_yz.
An exact proof term for the current goal is (SNo_mul_SNo dx_yz dx_yz Hdx_yzS Hdx_yzS).
We prove the intermediate claim Hdy2yzS: SNo dy2_yz.
An exact proof term for the current goal is (SNo_mul_SNo dy_yz dy_yz Hdy_yzS Hdy_yzS).
We prove the intermediate claim HAS: SNo A.
An exact proof term for the current goal is (SNo_add_SNo dx2_xy dy2_xy Hdx2xyS Hdy2xyS).
We prove the intermediate claim HBS: SNo B.
An exact proof term for the current goal is (SNo_add_SNo dx2_yz dy2_yz Hdx2yzS Hdy2yzS).
We prove the intermediate claim HdotS: SNo dot.
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo dx_xy dx_yz) (mul_SNo dy_xy dy_yz) (SNo_mul_SNo dx_xy dx_yz Hdx_xyS Hdx_yzS) (SNo_mul_SNo dy_xy dy_yz Hdy_xyS Hdy_yzS)).
We prove the intermediate claim HprodS: SNo prod.
An exact proof term for the current goal is (SNo_mul_SNo dxy dyz HdxyS HdyzS).
We prove the intermediate claim Hdxy2: mul_SNo dxy dxy = A.
We prove the intermediate claim HdxyDef: dxy = distance_R2 x y.
Use reflexivity.
rewrite the current goal using HdxyDef (from left to right).
rewrite the current goal using (distance_R2_sqr x y Hx Hy) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdyz2: mul_SNo dyz dyz = B.
We prove the intermediate claim HdyzDef: dyz = distance_R2 y z.
Use reflexivity.
rewrite the current goal using HdyzDef (from left to right).
rewrite the current goal using (distance_R2_sqr y z Hy Hz) (from left to right).
Use reflexivity.
We prove the intermediate claim HabsdotS: SNo (abs_SNo dot).
An exact proof term for the current goal is (SNo_abs_SNo dot HdotS).
We prove the intermediate claim HabsdotNN: 0 ≤ abs_SNo dot.
An exact proof term for the current goal is (abs_SNo_nonneg dot HdotS).
We prove the intermediate claim HprodNN: 0 ≤ prod.
An exact proof term for the current goal is (mul_SNo_nonneg_nonneg dxy dyz HdxyS HdyzS H0ledxy H0ledyz).
We prove the intermediate claim Hcs: mul_SNo dot dot ≤ mul_SNo A B.
An exact proof term for the current goal is (CauchySchwarz2_sq dx_xy dy_xy dx_yz dy_yz Hdx_xyS Hdy_xyS Hdx_yzS Hdy_yzS).
We prove the intermediate claim Hprod2: mul_SNo prod prod = mul_SNo A B.
We prove the intermediate claim HprodDef: prod = mul_SNo dxy dyz.
Use reflexivity.
rewrite the current goal using HprodDef (from left to right) at position 1.
rewrite the current goal using HprodDef (from left to right) at position 2.
We prove the intermediate claim Hdxy_dyzS: SNo (mul_SNo dxy dyz).
An exact proof term for the current goal is (SNo_mul_SNo dxy dyz HdxyS HdyzS).
rewrite the current goal using (mul_SNo_assoc dxy dyz (mul_SNo dxy dyz) HdxyS HdyzS Hdxy_dyzS) (from right to left).
rewrite the current goal using (mul_SNo_assoc dyz dxy dyz HdyzS HdxyS HdyzS) (from left to right).
rewrite the current goal using (mul_SNo_com dyz dxy HdyzS HdxyS) (from left to right).
rewrite the current goal using (mul_SNo_assoc dxy (mul_SNo dxy dyz) dyz HdxyS Hdxy_dyzS HdyzS) (from left to right).
rewrite the current goal using (mul_SNo_assoc dxy dxy dyz HdxyS HdxyS HdyzS) (from left to right).
rewrite the current goal using (mul_SNo_assoc (mul_SNo dxy dxy) dyz dyz (SNo_mul_SNo dxy dxy HdxyS HdxyS) HdyzS HdyzS) (from right to left).
rewrite the current goal using Hdxy2 (from left to right).
rewrite the current goal using Hdyz2 (from left to right).
Use reflexivity.
We prove the intermediate claim Habsdot2le: mul_SNo (abs_SNo dot) (abs_SNo dot) ≤ mul_SNo prod prod.
rewrite the current goal using (abs_SNo_sqr_eq dot HdotS) (from left to right).
rewrite the current goal using Hprod2 (from left to right).
An exact proof term for the current goal is Hcs.
We prove the intermediate claim HabsdotLe: abs_SNo dot ≤ prod.
An exact proof term for the current goal is (SNo_nonneg_sqr_Le_imp_Le (abs_SNo dot) prod HabsdotS HprodS HabsdotNN HprodNN Habsdot2le).
We prove the intermediate claim HdotLeAbs: dot ≤ abs_SNo dot.
Apply (xm (0 ≤ dot)) to the current goal.
Assume H0le: 0 ≤ dot.
rewrite the current goal using (nonneg_abs_SNo dot H0le) (from left to right).
An exact proof term for the current goal is (SNoLe_ref dot).
Assume Hn0le: ¬ (0 ≤ dot).
rewrite the current goal using (not_nonneg_abs_SNo dot Hn0le) (from left to right).
We prove the intermediate claim Hdotlt0: dot < 0.
Apply (SNoLt_trichotomy_or_impred dot 0 HdotS SNo_0 (dot < 0)) to the current goal.
Assume H: dot < 0.
An exact proof term for the current goal is H.
Assume Hdot0: dot = 0.
We prove the intermediate claim H0le0: 0 ≤ dot.
rewrite the current goal using Hdot0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
An exact proof term for the current goal is (FalseE (Hn0le H0le0) (dot < 0)).
Assume H0ltdot: 0 < dot.
We prove the intermediate claim H0ledot: 0 ≤ dot.
An exact proof term for the current goal is (SNoLtLe 0 dot H0ltdot).
An exact proof term for the current goal is (FalseE (Hn0le H0ledot) (dot < 0)).
We prove the intermediate claim Hdotle0: dot ≤ 0.
An exact proof term for the current goal is (SNoLtLe dot 0 Hdotlt0).
We prove the intermediate claim H0lemdot: 0 ≤ minus_SNo dot.
We prove the intermediate claim Hle: minus_SNo 0 ≤ minus_SNo dot.
An exact proof term for the current goal is (minus_SNo_Le_contra dot 0 HdotS SNo_0 Hdotle0).
rewrite the current goal using minus_SNo_0 (from right to left) at position 1.
An exact proof term for the current goal is Hle.
An exact proof term for the current goal is (SNoLe_tra dot 0 (minus_SNo dot) HdotS SNo_0 (SNo_minus_SNo dot HdotS) Hdotle0 H0lemdot).
We prove the intermediate claim HdotLeProd: dot ≤ prod.
An exact proof term for the current goal is (SNoLe_tra dot (abs_SNo dot) prod HdotS HabsdotS HprodS HdotLeAbs HabsdotLe).
We prove the intermediate claim Hdot2Le: add_SNo dot dot ≤ add_SNo prod prod.
An exact proof term for the current goal is (add_SNo_Le3 dot dot prod prod HdotS HdotS HprodS HprodS HdotLeProd HdotLeProd).
We prove the intermediate claim HrhsExp: mul_SNo s s = add_SNo (add_SNo A B) (add_SNo prod prod).
We prove the intermediate claim HsDef: s = add_SNo dxy dyz.
Use reflexivity.
rewrite the current goal using HsDef (from left to right).
rewrite the current goal using (SNo_foil dxy dyz dxy dyz HdxyS HdyzS HdxyS HdyzS) (from left to right).
rewrite the current goal using Hdxy2 (from left to right).
rewrite the current goal using Hdyz2 (from left to right).
rewrite the current goal using (mul_SNo_com dyz dxy HdyzS HdxyS) (from left to right).
rewrite the current goal using (add_SNo_assoc prod prod B HprodS HprodS HBS) (from left to right).
rewrite the current goal using (add_SNo_com (add_SNo prod prod) B (SNo_add_SNo prod prod HprodS HprodS) HBS) (from left to right).
rewrite the current goal using (add_SNo_assoc A B (add_SNo prod prod) HAS HBS (SNo_add_SNo prod prod HprodS HprodS)) (from right to left).
Use reflexivity.
We prove the intermediate claim HlhsExp: mul_SNo dxz dxz = add_SNo (add_SNo A B) (add_SNo dot dot).
We prove the intermediate claim HdxzDef2: dxz = distance_R2 x z.
Use reflexivity.
rewrite the current goal using HdxzDef2 (from left to right).
rewrite the current goal using (distance_R2_sqr x z Hx Hz) (from left to right).
rewrite the current goal using Hdx_decomp (from left to right).
rewrite the current goal using Hdy_decomp (from left to right).
rewrite the current goal using (SNo_foil dx_xy dx_yz dx_xy dx_yz Hdx_xyS Hdx_yzS Hdx_xyS Hdx_yzS) (from left to right).
rewrite the current goal using (SNo_foil dy_xy dy_yz dy_xy dy_yz Hdy_xyS Hdy_yzS Hdy_xyS Hdy_yzS) (from left to right).
rewrite the current goal using (mul_SNo_com dx_yz dx_xy Hdx_yzS Hdx_xyS) (from left to right).
rewrite the current goal using (mul_SNo_com dy_yz dy_xy Hdy_yzS Hdy_xyS) (from left to right).
We prove the intermediate claim Hdx2xyDef: dx2_xy = mul_SNo dx_xy dx_xy.
Use reflexivity.
We prove the intermediate claim Hdy2xyDef: dy2_xy = mul_SNo dy_xy dy_xy.
Use reflexivity.
We prove the intermediate claim Hdx2yzDef: dx2_yz = mul_SNo dx_yz dx_yz.
Use reflexivity.
We prove the intermediate claim Hdy2yzDef: dy2_yz = mul_SNo dy_yz dy_yz.
Use reflexivity.
We prove the intermediate claim HdotDef: dot = add_SNo (mul_SNo dx_xy dx_yz) (mul_SNo dy_xy dy_yz).
Use reflexivity.
We prove the intermediate claim HAdef: A = add_SNo dx2_xy dy2_xy.
Use reflexivity.
We prove the intermediate claim HBdef: B = add_SNo dx2_yz dy2_yz.
Use reflexivity.
rewrite the current goal using Hdx2xyDef (from right to left).
rewrite the current goal using Hdy2xyDef (from right to left).
rewrite the current goal using Hdx2yzDef (from right to left).
rewrite the current goal using Hdy2yzDef (from right to left).
rewrite the current goal using HdotDef (from right to left).
rewrite the current goal using HdotDef (from right to left).
rewrite the current goal using HAdef (from right to left).
rewrite the current goal using HAdef (from right to left).
rewrite the current goal using HBdef (from right to left).
rewrite the current goal using HBdef (from right to left).
We prove the intermediate claim Hdot2S: SNo (add_SNo dot dot).
An exact proof term for the current goal is (SNo_add_SNo dot dot HdotS HdotS).
rewrite the current goal using (add_SNo_assoc A B (add_SNo dot dot) HAS HBS Hdot2S) (from right to left).
We prove the intermediate claim HcrossxS: SNo (mul_SNo dx_xy dx_yz).
An exact proof term for the current goal is (SNo_mul_SNo dx_xy dx_yz Hdx_xyS Hdx_yzS).
We prove the intermediate claim HcrossyS: SNo (mul_SNo dy_xy dy_yz).
An exact proof term for the current goal is (SNo_mul_SNo dy_xy dy_yz Hdy_xyS Hdy_yzS).
We prove the intermediate claim Hcrossx_plus_dx2yzS: SNo (add_SNo (mul_SNo dx_xy dx_yz) dx2_yz).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo dx_xy dx_yz) dx2_yz HcrossxS Hdx2yzS).
We prove the intermediate claim Hcrossy_plus_dy2yzS: SNo (add_SNo (mul_SNo dy_xy dy_yz) dy2_yz).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo dy_xy dy_yz) dy2_yz HcrossyS Hdy2yzS).
We prove the intermediate claim HrestxS: SNo (add_SNo (mul_SNo dx_xy dx_yz) (add_SNo (mul_SNo dx_xy dx_yz) dx2_yz)).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo dx_xy dx_yz) (add_SNo (mul_SNo dx_xy dx_yz) dx2_yz) HcrossxS Hcrossx_plus_dx2yzS).
We prove the intermediate claim HrestyS: SNo (add_SNo (mul_SNo dy_xy dy_yz) (add_SNo (mul_SNo dy_xy dy_yz) dy2_yz)).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo dy_xy dy_yz) (add_SNo (mul_SNo dy_xy dy_yz) dy2_yz) HcrossyS Hcrossy_plus_dy2yzS).
rewrite the current goal using (add_SNo_com_4_inner_mid dx2_xy (add_SNo (mul_SNo dx_xy dx_yz) (add_SNo (mul_SNo dx_xy dx_yz) dx2_yz)) dy2_xy (add_SNo (mul_SNo dy_xy dy_yz) (add_SNo (mul_SNo dy_xy dy_yz) dy2_yz)) Hdx2xyS HrestxS Hdy2xyS HrestyS) (from left to right).
rewrite the current goal using HAdef (from right to left).
rewrite the current goal using (add_SNo_com_4_inner_mid (mul_SNo dx_xy dx_yz) (add_SNo (mul_SNo dx_xy dx_yz) dx2_yz) (mul_SNo dy_xy dy_yz) (add_SNo (mul_SNo dy_xy dy_yz) dy2_yz) HcrossxS Hcrossx_plus_dx2yzS HcrossyS Hcrossy_plus_dy2yzS) (from left to right).
rewrite the current goal using HdotDef (from right to left).
rewrite the current goal using (add_SNo_com_4_inner_mid (mul_SNo dx_xy dx_yz) dx2_yz (mul_SNo dy_xy dy_yz) dy2_yz HcrossxS Hdx2yzS HcrossyS Hdy2yzS) (from left to right).
rewrite the current goal using HdotDef (from right to left).
rewrite the current goal using HBdef (from right to left).
rewrite the current goal using (add_SNo_assoc dot dot B HdotS HdotS HBS) (from left to right).
rewrite the current goal using (add_SNo_com (add_SNo dot dot) B Hdot2S HBS) (from left to right).
Use reflexivity.
We prove the intermediate claim HmainLe: add_SNo (add_SNo A B) (add_SNo dot dot) ≤ add_SNo (add_SNo A B) (add_SNo prod prod).
An exact proof term for the current goal is (add_SNo_Le3 (add_SNo A B) (add_SNo dot dot) (add_SNo A B) (add_SNo prod prod) (SNo_add_SNo A B HAS HBS) (SNo_add_SNo dot dot HdotS HdotS) (SNo_add_SNo A B HAS HBS) (SNo_add_SNo prod prod HprodS HprodS) (SNoLe_ref (add_SNo A B)) Hdot2Le).
We prove the intermediate claim HdxzDef: dxz = distance_R2 x z.
Use reflexivity.
We prove the intermediate claim HdxyDef: dxy = distance_R2 x y.
Use reflexivity.
We prove the intermediate claim HdyzDef: dyz = distance_R2 y z.
Use reflexivity.
We prove the intermediate claim HsDef2: s = add_SNo dxy dyz.
Use reflexivity.
rewrite the current goal using Hdx_decomp (from right to left).
rewrite the current goal using Hdy_decomp (from right to left).
rewrite the current goal using (distance_R2_sqr x z Hx Hz) (from right to left).
rewrite the current goal using HdxzDef (from right to left).
rewrite the current goal using HdxyDef (from right to left).
rewrite the current goal using HdyzDef (from right to left).
rewrite the current goal using HsDef2 (from right to left).
rewrite the current goal using HlhsExp (from left to right).
rewrite the current goal using HrhsExp (from left to right).
An exact proof term for the current goal is HmainLe.
∎