prove of the simple problem of Fig. 1

I have tried the simple problem of Fig. 1, and it can be proved.

Is there anything wrong?

```
test
a b c = eq2_triangle a b c ? eqangle b c b a c a c b
```

where `eq2_triangle` is defined as:

```
eq2_triangle a b c
c : a b
=
a : ; b : ; c : cong a b a c
eq2_triangle
```

```python
def sketch_eq2_triangle(args: tuple[gm.Point, ...]) -> tuple[Point, ...]:
b = Point(0.0, 0.0)
c = Point(np.random.uniform(0.5, 1.0), 0)
a = Point((b.x + c.x) / 2, np.random.uniform(0.5, 10.0))
return a, b, c
```