A pedal triangle of a triangle ABC with respect to a point Q is defined as the triangle formed by the feet of the perpendiculars dropped on the sides of ABC from Q.
    The process of getting the pedal triangle can be extended to the pedal triangle itself, thus yielding pedal triangles of higher degree.Prove that the third pedal triangle of any triangle with respect to a point is similar to the triangle itself.

Machine input:
 

Point order : ABCQDEFGHLMNO

Hypothesis: coll(AFB) coll(BDC) coll(CEA) coll(EFG) coll(ELD) coll(FHD) coll(GMH) coll(GOL) coll(HNL) perp(QOGL) perp(QDBC) perp(QEAC) perp(QFAB) perp(QGFE) perp(QHFD) perp(QLDE) perp(QMGH) perp(QNHL)

Conclusion :  [NM,NQ] - [ON,NQ] - [CA,BA]  = 0

Machine output:
 

[NM,NQ] - [ON,NQ] - [CA,BA]
=   + [MH,HQ] - [ON,NQ] - [CA,BA]
        ( because cyclic(N,M,Q,H) => [NM,NQ] = [MH,HQ] )
=   + [MH,HQ] - [OL,LQ] - [CA,BA]
        ( because cyclic(O,N,Q,L) => -1.0[ON,NQ] = -1.0[OL,LQ] )
=  90.0 + [MQ,HQ] - [OL,LQ] - [CA,BA]
        ( because perp(M,H,M,Q) => [MH,HQ] = [MQ,HQ] + 90.0 )
=   + [HG,HQ] - [OL,LQ] - [CA,BA]
        ( because perp(M,Q,H,G) => [MQ,HQ] = [HG,HQ] + 90.0 )
=   + [GF,FQ] - [OL,LQ] - [CA,BA]
        ( because cyclic(H,G,Q,F) => [HG,HQ] = [GF,FQ] )
=  90.0 + [GQ,FQ] - [OL,LQ] - [CA,BA]
        ( because perp(G,F,G,Q) => [GF,FQ] = [GQ,FQ] + 90.0 )
=   + [FE,FQ] - [OL,LQ] - [CA,BA]
        ( because perp(G,Q,F,E) => [GQ,FQ] = [FE,FQ] + 90.0 )
=   + [EA,QA] - [OL,LQ] - [CA,BA]
        ( because cyclic(F,E,Q,A) => [FE,FQ] = [EA,QA] )
=  90.0 + [EA,QA] - [OQ,LQ] - [CA,BA]
        ( because perp(O,L,O,Q) => -1.0[OL,LQ] = -1.0[OQ,LQ] + -90.0 )
=   + [EA,QA] - [LG,LQ] - [CA,BA]
        ( because perp(O,Q,L,G) => -1.0[OQ,LQ] = -1.0[LG,LQ] + -90.0 )
=   + [EA,QA] - [GE,EQ] - [CA,BA]
        ( because cyclic(L,G,Q,E) => -1.0[LG,LQ] = -1.0[GE,EQ] )
=  90.0 + [EA,QA] - [GQ,EQ] - [CA,BA]
        ( because perp(G,E,G,Q) => -1.0[GE,EQ] = -1.0[GQ,EQ] + -90.0 )
=   + [EA,QA] - [FE,EQ] - [CA,BA]
        ( because perp(G,Q,F,E) => -1.0[GQ,EQ] = -1.0[FE,EQ] + -90.0 )
=   + [EA,QA] - [FA,QA] - [CA,BA]
        ( because cyclic(F,E,Q,A) => -1.0[FE,EQ] = -1.0[FA,QA] )
=   - [QA,CA] - [FA,QA] - [CA,BA]
        ( because parallel(E,A,C,A) => [EA,QA] = -1.0[QA,CA] )
=   - [QA,CA] + [QA,BA] - [CA,BA]
        ( because parallel(F,A,B,A) => -1.0[FA,QA] = [QA,BA] )
=  0.0
        ( because -1.0[QA,CA] = -1.0[QA,BA]+[CA,BA], simplifying )