Incorrect lean formalization in PB-Basic-028 and PB-Advanced-010

In PB-Basic-028, the statement "A circle W is tagent to the side AB at X" is translated as `W.IsTangentAt X (affineSpan R A, B)` in lean. The "side AB" should be interperet as the closed segment AB, not the line AB (`affineSpan R A,B`).
Losening the conditon admits a counterexample, see [benchmark-faithfulness-bugs.pdf](https://github.com/user-attachments/files/28870714/benchmark-faithfulness-bugs.pdf).

There is also a formalization issue when considering the degenerate case for PB-Advanced-010. Details and a counterexample are proivded in the attached pdf above.