[TYPES] A geometry problem for proof systems

[Yong Luo]

Hi,

The following geometry problem might be interesting for those who develop
proof systems based on type theory.

Property:  A triangle with two internal angle bisectors of equal length is
an isosceles triangle.

 More precisely, in a triangle ABC, the point D is on the line segment BC
and E on AC, and the line segments AD and BE are internal angle bisectors
(i.e. the angle CAD is equal to the angle DAB, and the angle ABE is equal to
EBC). If AD and BE are of equal length (AD=BE), then AC=BC.

If this property is not true, can we have a counter example? Is there anyone
interested in proving it in Coq or other systems ?

I asked myself this question in 1991, but I am not able to prove it even
now.

Thanks,

Yong

==============================
Dr. Yong Luo
Computing Laboratory
University of Kent