Prove that the orthocentre of a triangle is the incentre of the orthocentric pedal triangle.
(Orthocentric pedal triangle is the triangle formed by the feet of the perpendiculars of a triangle.)

Machine input:

Point order:ABCDEGF

Hypothesis: coll(AFB) coll(AEC) coll(BDC) coll(AGD) coll(BGE) coll(CGF) perp(ADBC) perp(ABCF) perp(ACBE)

Conclusion: [ADFD]-[ADED]=0

Machine output:

- [ED,DA] - [FD,DA]
=   - [EB,BA] - [FD,DA]
        ( because cyclic(E,D,A,B) => -1.0[ED,DA] = -1.0[EB,BA] )
=   - [EB,BA] - [FC,CA]
        ( because cyclic(F,D,A,C) => -1.0[FD,DA] = -1.0[FC,CA] )
= 90.0 - [CA,BA] - [FC,CA]
        ( because perp(E,B,C,A) => -1.0[EB,BA] = -1.0[CA,BA] + -90.0 )
= 0.0
        ( because perp(F,C,B,A) => -1.0[FC,CA] = [CA,BA] + -90.0 )