Nine point Circle:
Prove that the midpoints of the sides, the foot of the perpendiculars and the midpoints of the lines joining the vertices to the orthocentre, all lie on a circle.
(This circle is called as the nine point circle as the above nine points lie on it . )

Part 1:proving that the midpoints of the sides and the segments lie on a circle.

Machine input:

Point order: ABCDEFHP

Hypothesis: mid(DBC), mid(EAC), mid(FAB), orthocentre(HABC) mid(PHA)

Conclusion: cyclic(PFDE)

Machine output:

[PE,ED] - [PF,FD]
= 90.0 - [PF,FD]
because perp(P,E,E,D) => [PE,ED] = 90.0 )
= 0.0

because perp(P,F,F,D) => -1.0[PF,FD] = -90.0 )

Part 2: proving that the foot of the perpendiculars and the midpoint of the sides are concylic.

Machine input:

Point order : ABCDLMN

Hypothesis : coll(ALB) coll(ANC) coll(BDMC) mid(MBC) mid(NAC) mid(LAB) perp(ADBC)

Conclusion : Cyclic(DLMN)

Machine output:
- [NL,ND] + [ML,MD]
= 90.0 + [ND,DA] + [ML,MD]
        ( because perp(N,L,D,A) => -1.0[NL,ND] = [ND,DA] + -90.0 )
=   + [ND,CB] + [ML,MD]
        ( because perp(D,A,C,B) => [ND,DA] = [ND,CB] + 90.0 )
= 90.0 + [ND,CB] + [ML,DA]
        ( because perp(M,D,D,A) => [ML,MD] = [ML,DA] + 90.0 )
=   + [ND,CB] + [ML,CB]
        ( because perp(D,A,C,B) => [ML,DA] = [ML,CB] + 90.0 )
=   + [ND,CB] - [CB,CA]
        ( because parallel(M,L,C,A) => [ML,CB] = -1.0[CB,CA] )
=   - [NC,DC] - [CB,CA]
         (because [ND,CB] = -1.0[NC,DC] )
= 90.0 - [NC,DA] - [CB,CA]
        ( because perp(D,C,D,A) => -1.0[NC,DC] = -1.0[NC,DA] + -90.0 )
=   - [NC,CB] - [CB,CA]
        ( because perp(D,A,C,B) => -1.0[NC,DA] = -1.0[NC,CB] + -90.0 )
=   - [ML,CB] - [CB,CA]
        ( because parallel(N,C,M,L) => -1.0[NC,CB] = -1.0[ML,CB] )
= 0.0
         ( because parallel(M,L,C,A) => -1.0[ML,CB] = [CB,CA] )