Can I prove sth like AB=CD and AB=CD+EF?

[thedeepdeepsky]

Can I prove sth like AB=CD and AB=CD+EF?

[tpgh24]

For AB=CD just write ? cong A B C D. AlphaGeometry does not support goals like AB=CD+EF, but you can add a point say G on line CD with DG=EF, then prove cong A B C G. You cannot specify on which side of point D G falls, so it can be either CD+EF or CD-EF, but you will find that for many problems, the conclusion does not depend on the side of the point, so both points actual work. Also, AlphaGeometry will try to not let points overlap, so if there is already a point H between C and D with HD=EF, then when you construct G, it will be on the other side of D