Let p and c be given.
Assume Hp: p ∈ EuclidPlane.
Assume Hc: c ∈ EuclidPlane.
Assume Hlt: Rlt (distance_R2 p c) 0.
We prove the intermediate claim Hdlt0: distance_R2 p c < 0.
An exact proof term for the current goal is (RltE_lt (distance_R2 p c) 0 Hlt).
We prove the intermediate claim HdR: distance_R2 p c ∈ R.
An exact proof term for the current goal is (distance_R2_in_R p c Hp Hc).
We prove the intermediate claim HdS: SNo (distance_R2 p c).
An exact proof term for the current goal is (real_SNo (distance_R2 p c) HdR).
We prove the intermediate claim Hd0le: 0 ≤ distance_R2 p c.
An exact proof term for the current goal is (distance_R2_nonneg p c Hp Hc).
We prove the intermediate claim Hdle0: distance_R2 p c ≤ 0.
An exact proof term for the current goal is (SNoLtLe (distance_R2 p c) 0 Hdlt0).
We prove the intermediate claim Hd0: distance_R2 p c = 0.
An exact proof term for the current goal is (SNoLe_antisym (distance_R2 p c) 0 HdS SNo_0 Hdle0 Hd0le).
We prove the intermediate claim Hbad: 0 < 0.
rewrite the current goal using Hd0 (from right to left) at position 1.
An exact proof term for the current goal is Hdlt0.
An exact proof term for the current goal is ((SNoLt_irref 0) Hbad).
∎