Set s to be the term
add_SNo dxy dyz.
We prove the intermediate
claim HpairR:
s ∈ R ∧ dxz ∈ R.
An
exact proof term for the current goal is
(andEL (s ∈ R ∧ dxz ∈ R) (s < dxz) Hlt).
We prove the intermediate
claim Hslt:
s < dxz.
An
exact proof term for the current goal is
(andER (s ∈ R ∧ dxz ∈ R) (s < dxz) Hlt).
We prove the intermediate
claim HsumR:
s ∈ R.
An
exact proof term for the current goal is
(andEL (s ∈ R) (dxz ∈ R) HpairR).
We prove the intermediate
claim HxzR:
dxz ∈ R.
An
exact proof term for the current goal is
(andER (s ∈ R) (dxz ∈ R) HpairR).
We prove the intermediate
claim HdxyR:
dxy ∈ R.
We prove the intermediate
claim HdyzR:
dyz ∈ R.
We prove the intermediate
claim HdxzR:
dxz ∈ R.
An exact proof term for the current goal is HxzR.
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 HsS:
SNo s.
An
exact proof term for the current goal is
(SNo_add_SNo dxy dyz HdxyS HdyzS).
We prove the intermediate
claim H0ledxy:
0 ≤ dxy.
We prove the intermediate
claim H0ledyz:
0 ≤ dyz.
We prove the intermediate
claim H0les:
0 ≤ s.
rewrite the current goal using
(add_SNo_0L 0 SNo_0) (from right to left) at position 1.
We prove the intermediate
claim H0ledxz:
0 ≤ dxz.
An
exact proof term for the current goal is
(SNoLt_sqr_nonneg s dxz HsS HdxzS H0les H0ledxz Hslt).
∎