###########################################################
#RENE.txt: A MAPLE PACKAGE FOR STATING AND PROVING        #
#THEOREMS IN GEOMETRY; Save as RENE, go into              #
# Maple, and type:  read `RENE.txt`:                      #
###########################################################
 
#Written by Doron Zeilberger, Rutgers University 
#[zeilberg at math dot rutgers dot edu

 
#Version of Sept. 9, 2018 (To add  Miquel's Five Circle Theorem)
#Version of March 28, 2018 (To add Monthly problem P12027,March 2018, contrubuted by Dr. Z.'s Experimental Mathematics class)
#Version of  Feb. 6, 2012 (To add Monthly problem P11615,contributed by Matthew Russel, Rutgers University)
#Previous update: Feb. 10, 2011 (To add Monthly problem 11544, P11554)
#Oct. 14, 2004 (To add Sadov's theorem)
#May 5,  2001 (To add Monthly Problem P10874)
#Sept. 19, 2000 (TO adapt to Maple 6)
#Tested (1998) on Maple V, ver. 5 and below
#Thanks to Wolfram Koepf for pointing out that the previous version
#did not work on Maple V, ver. 5
#First Version Written: May 8, 1998
#Thanks: May 31, 1998 (thanks to Michael Somos for spotting a bug)
#The most current version is available from 
#http://www.math.temple.edu/~zeilberg/
 
 print(`RENE: A PACKAGE THAT USES RENE DESCARTES's`):
 print(`Revolutionary Approach to Geometry,`):
 print(`to state and prove 55 theorems in Plane Geometry`):
 print(``):
 print(`First Version Written: May 7, 1998`):
 print(`This version: Oct. 14, 2004 (to add Sadov's theorem)`):
 print(`Tested on Maple 9, ver. 5 and Maple 8`):
 print(`We benefited from a comment made by Wolfram Koepf and Michael Somos`):
 print(``):
 print(`written by Doron Zeilberger(zeilberg@math.temple.edu).`):
 print(`The most current version is always available from`):
 print(`http://www.math.temple.edu/~zeilberg/`):
 print(`For a list of the theorems type Theorems; `):
 print(`For a list of the definitions type : Definitions;`):
 print(`For a list of Monthly Problems type : MonthlyProblems;`):
 print(`For a list of IMO Problems type : IMO;`):
 print(`To see  a statment of a theorem, type:`):
 print(` op(Name_Of_Theorem);`):
 print(`To see  a statment of a defin., type:`):
 print( `op(Name_Of_Definition);`):
 print(`To prove a theorem, type: `):
 print(`Name_Of_Theorem();`);
 print():
 print(`For example, to see the statement of Napoleon's theorem type:`):
 print(`op(Napoleon); `):
 print(`To PROVE Napoleon's theorem, type: `):
 print(`Napoleon(); `):
 print(``):
 print(`Common abbreviations used in naming: Pt: Point; Le: Line;`):
 print(`Ce:Circle ; Te: Triangle ; De: Distance; Sq: Square; `):
 print(``):
 print(`Te(m,n): Gives the three vertices of the "standard trinagle",`):
 print(`whose vertices are A(0,0), B(1,0) and such that`):
 print(` m=tan((Angle CAB)/2), and n=tan((Angle CBA)/2) `):
 print(``):
 print(`Definition TS([A_1,A_2, ...])`):
 print(` expresses tan(arctan(A_1)+arctan(A_2)+...)`):
 print(` as a rational function of A_1,A_2, ...`):
 print(`Everything else is self-explanatory`):
 print(``):
 print(`TO SEE BEAUTIFUL DESCRIPTIONS, IN HUMANESE, OF MANY OF THE THEOREMS`):
 print(`PROVED HERE, CONSULT ERIC's TREASURE TROVE OF MATH`):
 print(``):
 print(`WARNING: x and y are GLOBAL VARIABLES DENOTING THE VARIABLES`):
 print(`DO NOT USE THEM FOR ANY OTHER PURPOSES, AND DO NOT ASSIGN THEM`):
 print(` Once Again:`):
 print(`For the list of Theorems type:`):
 print(`Theorems;`):
 print(`For the list of Definitions type:`):
 print(`Definitions;`):
 print(`For the list of Monthly Problems Solved type:MonthlyProblems;`):
 print(`For the list of International Math Olympiad Problems type:IMO;`):
 print(`To get a completely  self-contained statement AND proof of a theorem`):
 print(` Type "SelfContained(TheoremName);<CR>"; For example`):
 print(` e.g.: "SelfContained(Napoleon);<CR>"  `):
 
Theorems:=[AreaFormula,Bretschneider,Brianchon,Butterfly,Carnot,Casey,
CentroidExists,Ceva,Clifford,deLongchamps,Desargues,EightPointCircleExists,
Ekhad, EulerLineExists,EulerTetrahedronVolumeFormula,EulerTriangleFormula,
Feuerbach,FeuerbachConic,FinslerHadwiger,FoxTalbot,Fregier,Fuhrmann,Gergonne,
Griffiths,Herron,Hoehn,IncenterExists,Johnson,Lehmus,Lemoine,LeonAnne,
MarionMorgan, MedianTriangleLocus,Menelaus,MiquelFiveCircle, MiquelRandom,Monge,Morley,Napoleon,
NinePointCircleExists,Nobbs,OrthocenterExists,Pappus,Pascal,Pivot,Poncelet,
Ptolemy,Purser,RadicalCenterExists, Sadov, Simson,Soddy,Thebault,
Varignon,Viviani,vonAubel, Wittenbauer]:
 
Definitions:=[Altitude,AntiMedial,AREA,Billiard, BilliardSym,Ce,Center,
Centroid,CentroidQ,CET,Circumcenter,Circumradius,Colinear,ComTangLgt,
Concyclic,Concurrency,Concurrent,Contact,De,DePtLeSq,DeSq,DeSqG,EulerLine,Ft,
GegonnePt,Incenter,Incircle,Inradius,ItIsEqui,ItIsZero,Kiss,Le,MDOS,MidPt,
MirRefPtLe,MirRfPtPt,MirRefOf0,NinePointCircle,NormalToEllipse,Orthocenter,
OtherCeCe,ParamCircle,ParamLine,ParEllipse,Pedal,PerpMid,PerpPQ, pmidpt, Powe, 
Pt,PtLeCe,Quad,RadicalCenter, RadicalLine, Radius,Slope,Sqabc,SqRtABCD,
SSR,SSR1,Te,TS,Tangent,TangentToEllipse,TanMt,TouchCe,TouchCe1,TouchCeLe, 
TouchCeLe1,TcCesOut]:
 
MonthlyProblems:=[P10637,P10673, P10678, P10693, P10703,P10710,P10734,
P10749,P10780,P10783,P10796,P10804,P10810,P10845,P10874,P11554,
P11615, P12027]:
 
IMO:=[I78_4, I79_3, I82_2, I82_5]:
##########################Part I: THEOREMS############
 
AreaFormula:=proc() local A,B,C:
ItIsZero(DeSq(A,B)*DeSq(C,Ft(C,Le(A,B)))/4-AREA(A,B,C)^2):end:
 
Bretschneider:=proc() local A,B,C,D: ItIsZero(16*(AREA(A,B,C)+AREA(A,C,D))^2-
4*DeSq(A,C)*DeSq(B,D)+(DeSq(B,C)+DeSq(D,A)-DeSq(A,B)-DeSq(C,D))^2):end:
 
Brianchon:=proc() local Li,t,i,c,d,P: 
for i from 0 to 5 do Li[i]:=TangentToEllipse(c,d,t[i]): od: 
for i from 0 to 5 do P[i]:=Pt(Li[i],Li[i+1 mod 6]): od:
Concurrent(Le(P[0],P[3]),Le(P[1],P[4]),Le(P[2],P[5])):end:
 
Butterfly:=proc() local P,t,i,R,Li,M,X,Y:for i from 1 to 4 do 
P[i]:=ParamCircle([0,0],R,t[i]) od:M:=Pt(Le(P[1],P[3]),Le(P[2],P[4])):
Li:=PerpPQ([0,0],M):X:=Pt(Le(P[1],P[4]),Li):Y:=Pt(Le(P[2],P[3]),Li):
ItIsZero(DeSq(M,X)-DeSq(M,Y)):end:
 
Carnot:=proc() local m,n,T,O,O1,O2,O3,gu:T:=Te(m,n):O:=Circumcenter(T):
O1:=Ft(O,Le(T[2],T[3])):O2:=Ft(O,Le(T[1],T[3])):O3:=Ft(O,Le(T[1],T[2])):
SSR1([DeSq(O,O1),DeSq(O,O2),DeSq(O,O3)],Circumradius(T)-Inradius(m,n)):end:
 
Casey:=proc() local t,P,C,R,i,j:t[1]:=1: for i from 1 to 4 do 
P[i]:=ParamCircle([0,0],1,t[i]): od: for i from 1 to 4 do 
C[i]:=[(1-R[i])*P[i][1],(1-R[i])*P[i][2]]:od: for i from 1 to 4 do
for j from i+1 to 4 do t[i,j]:=simplify(
ComTangLgtSq(C[i],R[i],C[j],R[j])^2,symbolic): od:od:
SSR1([t[1,2]*t[3,4],t[1,3]*t[2,4],t[1,4]*t[2,3]],0):end:
 
CentroidExists:=proc() local A,B,C: 
Concurrent(Le(MidPt(A,B),C),Le(MidPt(A,C),B),Le(MidPt(B,C),A)):end:
 
Ceva:=proc() local A,B,C,O,D,E,F: A:=[0,0]: B:=[1,0]:
D:=Pt(Le(B,C),Le(A,O)):E:=Pt(Le(A,C),Le(B,O)):F:=Pt(Le(A,B),Le(C,O)):ItIsZero(
DeSq(B,D)*DeSq(C,E)*DeSq(A,F)-DeSq(D,C)*DeSq(E,A)*DeSq(F,B)): end:
 
#The Contact Triangle of the Standard Triangle Te(m,n)
Contact:=proc(m,n) local T,C:T:=Te(m,n):C:=Incenter(m,n):
Ft(C,Le(T[1],T[2])),Ft(C,Le(T[2],T[3])),Ft(C,Le(T[3],T[1])):end:
 
Clifford:=proc()local a,b,C,i,j,P,k: a[1]:=-2: b[1]:=0:
for i from 1 to 4 do C[i]:=x^2+y^2+a[i]*x+b[i]*y: od: for i from 1 to 4 do 
for j from i+1 to 4 do P[i,j]:=OtherCeCe(C[i],C[j],[0,0]):od:od: 
for i from 1 to 4 do for j from i+1 to 4 do  for k from j+1 to 4 do C[i,j,k]:=
Ce(P[i,j],P[i,k],P[j,k]):od:od:od:evalb(solve({C[1,2,3]-C[1,2,4],
C[1,2,3]-C[1,3,4],C[1,2,3]-C[2,3,4]},{x,y})<>NULL):end:
 
deLongchamps:=proc() local A,B,C,O,O1,O2,l: A:=[0,0]: B:=[1,0]:
O:=Circumcenter(A,B,C): O1:=Orthocenter(A,B,C):O2:=[O[1]-(O1[1]-O[1]),
O[2]-(O1[2]-O[2])]:l:=EulerLine(A,B,C):ItIsZero(subs({x=O2[1],y=O2[2]},l)):end:
 
Desargues:=proc() local A,B,i,m,t,s: for i from 1 to 3 do 
A[i]:=ParamLine(m[i],0,t[i]): B[i]:=ParamLine(m[i],0,s[i]):od: 
Colinear(Pt(Le(A[1],A[2]),Le(B[1],B[2])),Pt(Le(A[1],A[3]),Le(B[1],B[3])),
Pt(Le(A[2],A[3]),Le(B[2],B[3]))):end:
 
EightPointCircleExists:=proc() local A,B,C,D,e,f,g,h,a,b,c,d:
A:=[0,-e]:B:=[f,0]:C:=[0,g]:D:=[-h,0]:
a:=MidPt(A,B):b:=MidPt(B,C):c:=MidPt(C,D):d:=MidPt(D,A):Concyclic(
a,b,c,d,Ft(a,Le(C,D)),Ft(b,Le(D,A)),Ft(c,Le(A,B)),Ft(d,Le(B,C))):end:
  
EulerLineExists:=proc() local A,B,C: 
Colinear(Orthocenter(A,B,C),Circumcenter(A,B,C),Centroid(A,B,C)):end:

with(linalg): 
EulerTetrahedronVolumeFormula:=proc() local P1,P2,P3,P4,P,Q,R,A,B,C,Vol,
p31,p32,p41,p42,p43: 
P1:=[0,0,0]: P2:=[1,0,0]:P3:=[p31,p32,0]:
P4:=[p41,p42,p43]:P:=DeSqG(P1,P4,3):Q:=DeSqG(P2,P4,3):R:=DeSqG(P3,P4,3):
A:=DeSqG(P2,P3,3):B:=DeSqG(P3,P1,3):C:=DeSqG(P1,P2,3):
Vol:=AREA([p31,p32],[1,0],[0,0])*p43/3:evalb(normal(det(array([[0,P,Q,R,1],
[P,0,C,B,1],[Q,C,0,A,1],[R,B,A,0,1],[1,1,1,1,0]]))/Vol^2/288)=1):end:
 
EulerTriangleFormula:=proc() local T,m,n,A,B,C,d,R,r,O,I1: 
T:=Te(m,n):A:=T[1]:B:=T[2]:C:=T[3]:O:=Incenter(m,n):
I1:=Circumcenter(A,B,C):r:=Inradius(m,n):R:=Circumradius(A,B,C):
d:=sqrt(DeSq(O,I1)): ItIsZero((d^2-R^2)^2-4*r^2*R^2):end:
 
Feuerbach:=proc() local m,n:TouchCe(NinePointCircle(Te(m,n)),Incircle(m,n)):end:
 
FeuerbachConic:=proc() local O,B,C,D,E,F,Conic,c,d: O:=Orthocenter([0,0],[1,0],
[c,d]):Conic:=x^2+B*x*y+C*y^2+D*x+E*y+F:Conic:=subs(solve({subs({x=0,y=0},
Conic),subs({x=1,y=0},Conic),subs({x=c,y=d},Conic),subs({x=O[1],y=O[2]},Conic)},
{B,C,D,E,F}),Conic):ItIsZero(subs(solve({diff(Conic,x),diff(Conic,y)},{x,y}),
NinePointCircle([0,0],[1,0],[c,d]))):end:
 
FinslerHadwiger:=proc() local a,b,A,B,C,D,B1,C1,D1,Q,R,S,T:A:=[0,0]:B:=[-1,0]:
C:=[-1,1]:D:=[0,1]:B1:=[a,b]:C1:=[B1[1]+b,B1[2]-a]:D1:=[b,-a]:Q:=MidPt(D,B1):
S:=MidPt(B,D1):R:=Pt(Le(B,D),Le(A,C)):T:=Pt(Le(B1,D1),Le(A,C1)):evalb(
ItIsZero(DeSq(Q,T)-DeSq(T,S)) and ItIsZero(DeSq(Q,T)-DeSq(Q,R)) and 
ItIsZero(DeSq(Q,T)-DeSq(R,S)) and ItIsZero(Slope(Q,R)*Slope(Q,T)+1)):end:
 
FoxTalbot:=proc() local q,L,i,a,b,c,j,M: L[1]:=x: for  i from 2 to 5 do L[i]:=
a[i]*x+b[i]*y+c[i]: od: for i from 1 to 5 do  
q:=Quad(seq(L[j],j=1..i-1),seq(L[j],j=i+1..5)):M[i]:=Le(MidPt(q[1],q[3]),
MidPt(q[2],q[4])):od: Concurrent(seq(M[i],i=1..5)):end:
 
Fregier:=proc()local d,t,P,i,X,P2:for i from 0 to 2 do P[i]:=
ParEllipse([0,0],d,t[i]): od:  P[2]:=subs(t[2]=solve(Slope(P[0],P[1])*
Slope(P[0],P[2])=
-1,t[2]),P[2]):X:=Pt(NormalToEllipse([0,0],d,t[0]),Le(P[1],P[2])):
ItIsZero(normal(diff(X[1],t[1]))) and ItIsZero(normal(diff(X[1],t[2]))): end:
 
Fuhrmann:=proc() local P,Q,R,L,M,N,a,b,c,a1,b1,c1,e,f,g,t2,t3,t4,t5,t6,A,B,gu:
P:=ParamCircle([0,0],1,1):Q:=ParamCircle([0,0],1,t2):
R:=ParamCircle([0,0],1,t3):L:=ParamCircle([0,0],1,t4):
M:=ParamCircle([0,0],1,t5):N:=ParamCircle([0,0],1,t6):
a:=DeSq(L,M):b:=DeSq(R,Q):c:=DeSq(N,P):a1:=DeSq(P,Q):b1:=DeSq(M,N):
c1:=DeSq(L,R): e:=DeSq(R,N):f:=DeSq(L,P):g:=DeSq(M,Q):
SSR1([a*a1*e,b*b1*f,c*c1*g,a*b*c,a1*b1*c1,e*f*g],0):end:
 
Gergonne:=proc() local m,n,T,C1:T:=Te(m,n):C1:=Incircle(m,n):
Concurrent(Le(T[1],PtLeCe(Le(T[2],T[3]),C1)),Le(T[2],PtLeCe(Le(T[1],T[3]),C1)),
Le(T[3],PtLeCe(Le(T[1],T[2]),C1))):end:
 
Griffiths:=proc() local a,b,A,B,C,D,P,m,x1,c1,c2,g:A:=[0,0]:B:=[1,0]:C:=[a,b]:
D:=Circumcenter(A,B,C):P:=[D[1]+x1,D[2]+m*x1]:c1:=Ce(Pedal(A,B,C,P)):
c2:=NinePointCircle(A,B,C): g:=numer(factor(subs(y=solve(c1-c2,y),c2))):
evalb(type(g,`*`) and (diff(op(1,g),x1)=0 or diff(op(2,g),x1)=0)):end:
 
Herron:=proc() local q,a,b,c,s,A,B,C,b1,a2,b2,Area:A:=[0,0]:B:=[0,b1]:
C:=[a2,b2]:a:=sqrt(DeSq(B,C)):b:=sqrt(DeSq(A,C)):c:=sqrt(DeSq(A,B)):
s:=(a+b+c)/2: ItIsZero(AREA(A,B,C)^2-s*(s-a)*(s-b)*(s-c)):end:
 
Hoehn:=proc()  local V1,V2,V3,V4,V5,W1,W2,W3,W4,W5:V1:=[0,0]:V2:=[1,0]:
W1:=Pt(Le(V1,V3),Le(V2,V5)):W2:=Pt(Le(V1,V3),Le(V2,V4)):W3:=Pt(Le(V3,V5),
Le(V2,V4)):W4:=Pt(Le(V1,V4),Le(V3,V5)):W5:=Pt(Le(V1,V4),Le(V2,V5)):
ItIsZero(DeSq(V1,W1)*DeSq(V2,W2)*DeSq(V3,W3)*DeSq(V4,W4)*DeSq(V5,W5)-
DeSq(V1,W5)*DeSq(V2,W1)*DeSq(V3,W2)*DeSq(V4,W3)*DeSq(V5,W4)):end:
 
IncenterExists:=proc() local m,n,A,B,C,T:T:=Te(m,n):A:=T[1]:B:=T[2]:
C:=T[3]:Concurrent(y-m*x,y+n*x-n,y-C[2]-(x-C[1])*TS(m,1/n)):end:
 
Johnson:=proc() local C,t,i,R,P: for i from 0 to 2 do C[i]:=ParamCircle(
[0,0],R,t[i]): od: for i from 0 to 2 do P[i]:=MirRefOf0(C[i],C[i+1 mod 3]) : 
od: ItIsZero(Radius(Ce(P[0],P[1],P[2]))^2-R^2): end:
 
Lehmus:=proc() local N,M,m,n:N:=Pt(y-TS(m,m)*x,y+n*(x-1)):
M:=Pt(y-m*x,y+TS(n,n)*(x-1)):
ItIsZero(subs(m=n,factor(DeSq([1,0],N)-DeSq([0,0],M)))):end:
 
Lemoine:=proc() local m,n,T,A,B,C,G:T:=Te(m,n):A:=T[1]:B:=T[2]:C:=T[3]:G:=
Centroid(T):Concurrent(MirRefLeLe(Le(A,G),y-m*x),MirRefLeLe(Le(B,G),y+n*x-n),
MirRefLeLe(Le(C,G),y-C[2]-expand((x-C[1])*TS(m,1/n)))):end:
 
LeonAnne:=proc() local A,B,C,D,O1,l,x1: 
l:=Le(MidPt(A,C),MidPt(B,D)):O1:=[x1,subs(x=x1,solve(l,y))]:
ItIsZero(1/2-(AREA(A,B,O1)+AREA(C,D,O1))/(AREA(A,B,C)+AREA(A,C,D) )):end:
 
#The Morgan generalization of Marion Walter's Theorem
MarionMorgan:=proc() local a,b,n,A,B,C,A1,A2,B1,B2,C1,C2,P1,P2,P3,P4,P5,P6:
A:=[0,0]: B:=[1,0]: C:=[a,b]:
C1:=pmidpt(A,B,n/(2*n+1)):C2:=pmidpt(A,B,(n+1)/(2*n+1)):
A1:=pmidpt(B,C,n/(2*n+1)):A2:=pmidpt(B,C,(n+1)/(2*n+1)):
B1:=pmidpt(C,A,n/(2*n+1)):B2:=pmidpt(C,A,(n+1)/(2*n+1)):
P1:= Pt(Le(A,A1),Le(B,B2)):P2:= Pt(Le(A,A1),Le(C,C2)):P3:=Pt(Le(B,B1),Le(C,C2)):
P4:=Pt(Le(B,B1),Le(A,A2)):P5:=Pt(Le(C,C1),Le(A,A2)):P6:=Pt(Le(C,C1),Le(B,B2)):
ItIsZero((AREA(P1,P2,P3)+AREA(P1,P3,P4)+AREA(P1,P4,P5)+
AREA(P1,P5,P6))/AREA(A,B,C)-2/(3*n+1)/(3*n+2)):
end:
 
MedianTriangleLocus:=proc() local s,p,A,B,C,T,R,P,Q,a,b,c,m,n,gu: 
T:=AntiMedial(Te(m,n)):A:=T[1]:B:=T[2]:C:=T[3]:R:=Pedal(Te(m,n),Incenter(m,n)):
c:=-sqrt(factor(DeSq(A,B))):b:=-sqrt(factor(DeSq(A,C))): 
a:=sqrt(factor(DeSq(C,B))):s:=normal((a+b+c)/2):
P:=[A[1]+(p/c)*(B[1]-A[1]),A[2]+(p/c)*(B[2]-A[2])]:Q:=[A[1]+((s-p)/b)*
(C[1]-A[1]),A[2]+((s-p)/b)*(C[2]-A[2])]:
gu:=AREA(R[2],R[3],MidPt(P,Q)):gu:=simplify(gu,symbolic):gu:=simplify(gu):
ItIsZero(gu):end:
 
Menelaus:=proc() local A,B,C,X,Y,Z,L,m,b: L:=y-m*x-b: X:=Pt(Le(B,C),L):
Y:=Pt(Le(A,C),L):Z:=Pt(Le(A,B),L):ItIsZero(
DeSq(B,X)*DeSq(C,Y)*DeSq(A,Z)-DeSq(C,X)*DeSq(A,Y)*DeSq(B,Z)): end:
 
Miquel:=proc() local r,A,P,C,t,i,s:
print(`This is too big for Maple, so it is here for the future versions`):
print(`Meanwhile try MiquelRandom();`):
for i from 0 to 3 do A[i]:=ParamCircle([0,0],1,t[i]): od:
for i from 0 to 3 do C[i]:=ParPtPerBisect(A[i],A[(i+1) mod 4],s[i]): od:
for i from 0 to 3 do P[i]:=MirRefPtLe(A[i],Le(C[(i-1) mod 4],C[i])):od:
Concyclic(P[0],P[1],P[2],P[3]):end:
 
MiquelRandom:=proc() local r,A,P,C,t,i,s:print(`This is too big for Maple`):
print(`Hence, let's pick random values, giving an empirical proof`):
r:=rand(1..1000):
for i from 0 to 3 do t[i]:=r():s[i]:=r():od:
for i from 0 to 3 do A[i]:=ParamCircle([0,0],1,t[i]): od:
for i from 0 to 3 do C[i]:=ParPtPerBisect(A[i],A[(i+1) mod 4],s[i]): od:
for i from 0 to 3 do P[i]:=MirRefPtLe(A[i],Le(C[(i-1) mod 4],C[i])):od:
print(`Miquel's theorem is (empirically)`):Concyclic(P[0],P[1],P[2],P[3]):end:
 
Monge:=proc() local d1,d2,C1,C3,R1,R2,R3,a,b:d1:=sin1(b)/sin1(a*b):
d2:=sin1(a)/sin1(a*b): C1:=[0,0]: C3:=[d1*cos1(a),d1*sin1(a)]:
Colinear(TanMt(C1,R1,a,d1,R3),TanMt(C3,R3,1/b,d2,R2),TanMt(C1,R1,1,1,R2)):end:
 
Morley:=proc() local m,n,A,B,C,D,E,F:A:=[0,0]:B:=[1,0]: 
C:=Pt(y-TS(m,m,m)*x,y+TS(n,n,n)*(x-1)):D:=Pt(y-m*x,y+n*x-n):
E:=Pt(y-TS(m,m)*x,y-C[2]-(x-C[1])*TS(m,m,-n,sqrt(3))):
F:=Pt(y+TS(n,n)*(x-1),y-C[2]+(x-C[1])*TS(n,n,-m,sqrt(3))):ItIsEqui(D,E,F):end:
 
Nagel:=proc() local m,n,T:T:=Te(m,n):Concurrent(
Le(T[1],PtLeCe(Le(T[2],T[3]),Incircle(m,-1/n))),
Le(T[2],PtLeCe(Le(T[1],T[3]),Incircle(-1/m,n))),
Le(T[3],PtLeCe(Le(T[1],T[2]),Incircle(-1/m,-1/n)))):end:
 
Napoleon:=proc() local A,B,C: ItIsEqui(CET(A,B),CET(B,C),CET(C,A)): end:
 
NinePointCircleExists:=proc() local A,B,C,O,D,E,F,G,H,I1,K,L,M:
D:=Ft(A,Le(B,C)):E:=Ft(B,Le(A,C)):F:=Ft(C,Le(A,B)):
G:=MidPt(A,B):H:=MidPt(A,C):I1:=MidPt(B,C):O:=Orthocenter(A,B,C):
K:=MidPt(O,A):L:=MidPt(O,B):M:=MidPt(O,C):Concyclic(D,E,F,G,H,I1,K,L,M):end:
 
Nobbs:=proc() local m,n,T,S:T:=Te(m,n):S:=Contact(m,n):
Colinear(Pt(Le(T[1],T[2]),Le(S[2],S[3])),Pt(Le(T[2],T[3]),Le(S[3],S[1])),
Pt(Le(T[3],T[1]),Le(S[1],S[2]))):end:
 
OrthocenterExists:=proc() local A,B,C:
Concurrent(Altitude(A,Le(B,C)),Altitude(B,Le(A,C)),Altitude(C,Le(A,B))):end:
 
Pappus:=proc() local t,s,m,b,m1,b1,i,P,Q:
for i from 1 to 3 do P[i]:=ParamLine(m,b,t[i]): Q[i]:=ParamLine(m1,b1,s[i]): od:
Colinear(Pt(Le(P[1],Q[2]),Le(P[2],Q[1])),Pt(Le(P[1],Q[3]),Le(P[3],Q[1])),
Pt(Le(P[2],Q[3]),Le(P[3],Q[2]))):end:
 
Pascal:=proc() local c,d,s,t,i,P,Q: for i from 1 to 3 do P[i]:=ParEllipse(
c,d,t[i]):Q[i]:=ParEllipse(c,d,s[i]):od:Colinear(Pt(Le(P[1],Q[2]),Le(P[2],Q[1])),
Pt(Le(P[1],Q[3]),Le(P[3],Q[1])),Pt(Le(P[2],Q[3]),Le(P[3],Q[2]))):end:
 
Pivot:=proc() local A,B,C,A1,B1,C1,t1,t2,t3,P1,P2: A:=[0,0]: B:=[1,0]:
A1:=[t1*B[1]+(1-t1)*C[1],t1*B[2]+(1-t1)*C[2]]:
B1:=[t2*C[1]+(1-t2)*A[1],t2*C[2]+(1-t2)*A[2]]:
C1:=[t3*A[1]+(1-t3)*B[1],t3*A[2]+(1-t3)*B[2]]:
P1:=OtherCeCe(Ce(A,B1,C1),Ce(B,A1,C1),C1):
P2:=OtherCeCe(Ce(B,A1,C1),Ce(C,A1,B1),A1):
evalb(normal([expand(P1[1]-P2[1]),expand(P1[2]-P2[2])])=[0,0]): end:
 
Poncelet:=proc() local t0,t1,t2,t3,A,B,C,t,R,Q,Q1,Q2,P,c,L1,L2,L3,eq: 
L1:=TangentToEllipse([0,0],[1,1],t1):L2:=TangentToEllipse([0,0],[1,1],t2):
L3:=TangentToEllipse([0,0],[1,1],t3):L1:=subs(t1=1,L1):A:=Pt(L1,L2):
B:=Pt(L1,L3):C:=Pt(L2,L3):R:=Circumradius(A,B,C):c:=Circumcenter(A,B,C):
R:=simplify(R,symbolic): P:=ParamCircle(c,R,t0):Q:=ParamCircle(c,R,t):
eq:=solve(TouchCeLe1(x^2+y^2-1,Le(P,Q)),t):Q1:=subs(t=eq[1],Q):
Q2:=subs(t=eq[2],Q):TouchCeLe(x^2+y^2-1,Le(Q1,Q2)):end:
 
Ptolemy:=proc() local P,i,t,R: for i from 1 to 4 do 
P[i]:=ParamCircle([0,0],R,t[i]): od: Sqabc(DeSq(P[1],P[2])*DeSq(P[3],P[4]),
DeSq(P[2],P[3])*DeSq(P[4],P[1]),DeSq(P[1],P[3])*DeSq(P[2],P[4])):end:
 
Purser:=proc() local r,t1,t2,t3,A,B,C,a,b,c,u,v,t,M,f,X,Y:
A:=ParamCircle([0,0],1,t1):B:=ParamCircle([0,0],1,t2):
C:=ParamCircle([0,0],1,t3):M:=[1+r,0]:a:=DeSq(B,C):b:=DeSq(A,C):c:=DeSq(A,B):
v:=DeSq(C,M)-r^2:u:=DeSq(B,M)-r^2: t:=DeSq(A,M)-r^2:
f:=SSR(X,3,Y): evalb(expand(subs({X[1]=a*t,X[2]=b*u,X[3]=c*v,Y=0},f))=0):end:
 
RadicalCenterExists:=proc() local C,R:
Concurrent(RadicalLine(C[1],R[1],C[2],R[2]),RadicalLine(C[1],R[1],C[2],R[2]),
RadicalLine(C[3],R[3],C[3],R[3])):end:

#Sadov's Cubic analog of Ptolemy: (arXiv:math.GM/0410234 v1, 8 Oct. 2004)
#if a,b,c,d are the side-
#lentghs of a quadrilateral inscribed in a circle, and p,q
#are the diagonal lengths, then abp+cdp=bcq+adq
Sadov:=proc() local t1,t2,t3,t4,A,B,C,D,a,b,c,d,p,q: 
A:=ParamCircle([0,0],1,t1): B:=ParamCircle([0,0],1,t2):
C:=ParamCircle([0,0],1,t3): D:=ParamCircle([0,0],1,t4):
a:=DeSq(A,B):b:=DeSq(B,C):c:=DeSq(C,D):
d:=DeSq(D,A):p:=DeSq(A,C):q:=DeSq(B,D):

SqRtABCD(a*b*p,c*d*p,b*c*q,a*d*q):
end:
 
Simson:=proc() local t,i,P,R:for i from 1 to 4 do  
P[i]:=ParamCircle([0,0],R,t[i]): od: Colinear(Ft(P[4],Le(P[1],P[2])),
Ft(P[4],Le(P[2],P[3])),Ft(P[4],Le(P[3],P[1]))):end:

with(grobner): 
Soddy:=proc() local q,e1,e2,e3,e4,c,d,e,TC,R,r,s,t,p:
R:=1:TC:=TcCesOut:c:=[r+R,0]:q:=gbasis({TC(c,r,d,s),TC(c,r,e,t),TC(d,s,e,t),
TC([0,0],R,c,r),TC([0,0],R,d,s),TC([0,0],R,e,t)},[d[1],e[1],d[2],e[2],r,s,t],
tdeg):e4:=1/R:e1:=1/r:e2:=1/s:e3:=1/t:
p:=-2*(e1^2+e2^2+e3^2+e4^2)+(e1+e2+e3+e4)^2:p:=numer(normal(p)):
ItIsZero(normalf(p,q,[d[1],e[1],d[2],e[2],r,s,t],tdeg)):end:
Thebault:=proc() local m,n,t,p1,p2, I1,T,A,M,eq1,eq2,lu,Ci,Ci1,i,j,SOL,lua:
T:=Te(m,n):A:=T[3]:I1:=Incenter(m,n):M:=[t,0]:
Ci:=Ce(T): Ci1:=(x-p1)^2+(y-p2)^2-p2^2:
eq1:=TouchCe1(Ci1,Ci): lu:=solve(eq1,p2):
if subs({m=1/3,n=1/3,t=1/2,p1=1/2},lu[1])>0 then lu:=lu[1]: else  
lu:=lu[2]: fi:
eq2:=TouchCeLe1(Ci1,Le(A,M)): eq2:=numer(normal(subs(p2=lu,eq2))):
lua:=solve(eq2,p1):
SOL:=[seq([lua[i], subs(p1=lua[i],lu)],i=1..nops([lua]))]:
for i from 1 to nops(SOL) do
for j from i+1 to nops(SOL) do
if Colinear(I1,SOL[i],SOL[j]) then
RETURN(true):
fi:
od:
od:
false:
end:
 
Varignon:=proc()  local A,M,i: for i from 0 to 3 do M[i]:=
MidPt(A[i],A[i+1 mod 4]) od:ItIsZero(Slope(M[0],M[1])-Slope(M[2],M[3])) and 
ItIsZero(Slope(M[1],M[2])-Slope(M[3],M[0])):end:
 
Viviani:=proc() local A,B,C,T,P,f,X,Y: T:=Te(1/sqrt(3),1/sqrt(3)):
A:=T[1]:B:=T[2]:C:=T[3]:f:=SSR(X,3,Y):
ItIsZero(subs({X[1]=DeSq(P,Ft(P,Le(A,B))),X[2]=DeSq(P,Ft(P,Le(A,C))),
X[3]=DeSq(P,Ft(P,Le(B,C))),Y=sqrt(DeSq(C,Ft(C,Le(A,B))))},f)):end:
 
vonAubel:=proc() local A,B,C,D,P,Q,R,S: 
P:=MDOS(A,B):Q:=MDOS(B,C):R:=MDOS(C,D):S:=MDOS(D,A):
ItIsZero(Slope(P,R)*Slope(Q,S)+1) and ItIsZero(DeSq(P,R)-DeSq(Q,S)):end:
 
Wittenbauer:=proc() local A,P,l,i: for i from 0 to 3 do
l[i]:=Le([(2/3)*A[i][1]+1/3*A[i+1 mod 4][1],(2/3)*A[i][2]+1/3*A[i+1 mod 4][2]],
[(2/3)*A[i][1]+1/3*A[i-1 mod 4][1],(2/3)*A[i][2]+1/3*A[i-1 mod 4][2]]):od: 
for i from 0 to 3 do P[i]:=Pt(l[i],l[i+1 mod 4]): od:evalb(normal(
Pt(Le(P[0],P[2]),Le(P[1],P[3])))=normal(CentroidQ(A[0],A[1],A[2],A[3]))):end:
 
########################PART II:DEFINITIONS##########################
 
#Def (The perpendicular to line Le1 that passes through point Pt1
Altitude:=proc(Pt1,Le1): expand(coeff(expand(Le1),x,1)*(y-Pt1[2])-
coeff(expand(Le1),y,1)*(x-Pt1[1])): end:
 
#The triangle whose medial triangle is DEF
AntiMedial:=proc(D,E,F) local A,B,C,eq,var:eq:={D[1]=(A[1]+B[1])/2,D[2]=
(A[2]+B[2])/2,E[1]=(A[1]+C[1])/2,E[2]=(A[2]+C[2])/2,F[1]=(B[1]+C[1])/2,F[2]=
(B[2]+C[2])/2}:var:={A[1],B[1],C[1],A[2],B[2],C[2]}: var:=solve(eq,var):
subs(var,[A[1],A[2]]),subs(var,[B[1],B[2]]),subs(var,[C[1],C[2]]):end:
 
#Def(Area of triangle ABC)
AREA:=proc(A,B,C):normal(expand((B[1]*C[2]-B[2]*C[1]-A[1]*C[2]+A[2]*C[1]
-B[1]*A[2]+B[2]*A[1])/2)):end:
 
#Def The refl. of  line L1 through line L2
Billiard:=proc(L1,L2) local gu,L1a,L2a,a,b,c,d,e,f:
L1a:=a*x+b*y+c:L2a:=d*x+e*y+f:gu:=BilliardSym(L1a,L2a):
subs({a=coeff(expand(L1),x,1),b=coeff(expand(L1),y,1),c=subs(y=0,subs(x=0,L1)),
d=coeff(expand(L2),x,1),e=coeff(expand(L2),y,1),f=subs(y=0,subs(x=0,L2))},gu):
end:
 
#Def (The refl. of gen. line L1 through gen. line L2)
BilliardSym:=proc(L1,L2) local P,m,n,sl:
m:=-coeff(L1,x,1)/coeff(L1,y,1):n:=-coeff(L2,x,1)/coeff(L2,y,1):
P:=Pt(L1,L2): sl:=TS(n,n,-m):numer(normal((y-P[2])-sl*(x-P[1]))):end:
 
#Def (The Circumcircle of the inputed Points)
Ce:=proc() local eq,a,b,c,i,q:eq:=x^2+y^2+a*x+b*y+c:q:=solve({seq(subs(
{x=args[i][1],y=args[i][2]},eq),i=1..nargs)}  ,{a,b,c}):expand(subs(q,eq)):end:
 
#Def(The Center of a Circle Circ)
Center:=proc(Circ):
normal([-coeff(expand(Circ),x,1)/2,-coeff(expand(Circ),y,1)/2]):end:
 
#Def (The intersection of the three medians)
Centroid:=proc(A,B,C):Concurrency(Le(MidPt(A,B),C),Le(MidPt(A,C),B),
Le(MidPt(B,C),A)):end:
 
#The centroid of the quadrilateral ABCD
CentroidQ:=proc(A,B,C,D) local P,Q,a,b:P:=Centroid(A,B,C):Q:=Centroid(A,C,D):
a:=AREA(A,B,C): b:=AREA(A,C,D):
[a/(a+b)*P[1]+b/(a+b)*Q[1],a/(a+b)*P[2]+b/(a+b)*Q[2]]:end:
 
#Def(Circumcenter of the equilateral triangle two of whose vertices are A and B)
CET:=proc(A,B):Circumcenter(A, B, [(B[1]+A[1])/2-(A[2]-B[2])*3^(1/2)/2, 
B[2]/2+(A[1]-B[1])*3^(1/2)/2+A[2]/2]):end:
 
#Def (The Circumcenter of the triangle ABC)
Circumcenter:=proc(A,B,C):Center(Ce(A,B,C)):end:
 
#Def (Circumradius of the triangle ABC)
Circumradius:=proc(A,B,C):radsimp(Radius(Ce(A,B,C))):end:
 
#Def (The inputed points all on the same line?)
Colinear:=proc() local i: 
if nargs<2 then ERROR(`Need at least two Pts`): fi: for i from 3 to nargs do
if AREA(args[1],args[2],args[i])<>0 then  RETURN(false):fi:od:true:end:
 
#Length of a common tangent to the circles centered C1(C2) with radius R1(R2)
ComTangLgtSq:=proc(C1,R1,C2,R2) local a,d:d:=sqrt(DeSq(C1,C2)):a:=d*R2/(R1-R2):
sqrt((d+a)^2-R1^2)-sqrt(a^2-R2^2):end:
 
#Def (Are the inputed points all on the same circle?)
Concyclic:=proc() local i,C1:C1:=Ce(args[1],args[2],args[3]):
for i from 4 to nargs do if not ItIsZero(C1-Ce(args[1],args[2],args[i])) then 
RETURN(false): fi: od: true: end:
 
#Def (The common point of the inputed lines)
Concurrency:=proc() local q: q:=solve({args},{x,y}):[subs(q,x),subs(q,y)]: end:
 
#Def (Are the inputed lines concurrent?)
Concurrent:=proc(): not evalb(solve({args},{x,y})=NULL): end:
 
#Def (the distance between point A and point B) (use with caution)
De:=proc(A,B):sqrt(DeSq(A,B)):end:
 
#Def (Square of Distance of point P to line L)
DePtLeSq:=proc(P,L):DeSq(Pt(Altitude(P,L),L),P):end:
 
#Def (The square of the distance of points A and B)
DeSq:=proc(A,B):(A[1]-B[1])^2+(A[2]-B[2])^2: end:
 
#Def (The square of the distance of points A and B, in dim-dimensional space)
DeSqG:=proc(A,B,dim) local i :sum((A[i]-B[i])^2,i=1..dim): end:
 
#Def(Excircles of standard triangle Te(m,n)
Excircles:=proc(m,n) local C,T,a,b,c,gu,i: T:=Te(m,n):C:=x^2+y^2+a*x+b*y+c: 
gu:=solve({TouchCeLe1(C,Le(T[1],T[2])),TouchCeLe1(C,Le(T[1],T[3])),
TouchCeLe1(C,Le(T[2],T[3]))},{a,b,c}):
{seq(subs(gu[i],C),i=1..nops([gu]))} minus {Incircle(m,n)}:end:
 
#Def (The line through Circumcenter, Orthocenter, and Centroid)
EulerLine:=proc(A,B,C):Le(Orthocenter(A,B,C),Circumcenter(A,B,C)):end:
 
#Def (Projection of point Pt1 on line Le1)
Ft:=proc(Pt1,Le1) :Pt(Altitude(Pt1,Le1),Le1):end:
 
#Def (Gergonne Point of Standard Triangle Te(m,n))
GergonnePt:=proc(m,n) local T,C1:T:=Te(m,n):C1:=Incircle(m,n):
Pt(Le(T[1],PtLeCe(Le(T[2],T[3]),C1)),Le(T[2],PtLeCe(Le(T[1],T[3]),C1))):end:
 
 
#Def(The incenter of the triangle whose vertices are A(0,0), B(1,0),
#and the slopes of AB and BC are TS(m,m),TS(n,n),resp.)
 
Incenter:=proc(m,n) local C: C:=Te(m,n)[3]: if m=n then [1/2,m/2] :else 
Concurrency(y-m*x,y+n*x-n,y-C[2]-expand((x-C[1])*TS(m,1/n))) fi:end:
 
#Def: The eq. of the incircle through the standard triangle
Incircle:=proc(m,n) local C,R:R:=Inradius(m,n):C:=Incenter(m,n):
expand((x-C[1])^2+(y-C[2])^2-R^2):end:
 
#Def(The inradius of the standard triangle )
Inradius:=proc(m,n) local A,B,C,T,O:
T:=Te(m,n):A:=T[1]:B:=T[2]:C:=T[3]:O:=Incenter(m,n):
radsimp(sqrt(normal({DePtLeSq(O,Le(A,B)),DePtLeSq(O,Le(A,C)),DePtLeSq(O,Le(B,C))})[1])):
end:
 
#Def(Is the triangle ABC equilateral?)
ItIsEqui:=proc(A,B,C):evalb(normal
({DeSq(A,B)-DeSq(A,C),DeSq(B,C)-DeSq(C,A)})={0}):end:
 
#Def(Is it zero?)
ItIsZero:=proc(a):evalb(normal(a)=0):end:
 
#Kiss(Pt1,Pt2,Ce1): The point P, that lies on Ce1, and such that
#the Circle through Pt1,Pt2,P touches Ce1 at P
Kiss:=proc(Pt1,Pt2,Ce1) local x1,y1,gu1,gu2,lu,Pt3:
gu1:=Tangent(Ce1,[x1,y1]):gu2:=Tangent(Ce(Pt1,Pt2,[x1,y1]),[x1,y1]):
lu:=solve({subs({x=x1,y=y1},Ce1),coeff(gu2,x,1)*coeff(gu1,y,1)-
coeff(gu1,x,1)*coeff(gu2,y,1)},{x1,y1}): Pt3:=subs(lu[1],[x1,y1]):
if not Colinear(Pt1,Pt2,Pt3) then RETURN(Pt3): else 
RETURN(subs(lu[2],[x1,y1])): fi: end:
 
#Def (The eq. of the line joining A and B)
Le:=proc(A,B) AREA(A,B,[x,y]):end:
 
#MDOS(A,B): The point where the diagonals of the Outside Square on AB meet
MDOS:=proc(A,B) local a,b: a:=B[1]-A[1]:b:=B[2]-A[2]:
Pt(Le(A,[A[1]+a+b,A[2]+b-a]),Le(B,[A[1]+b,A[2]-a])):end:
 
#Def (The midpoint between A and B)
MidPt:=proc(A,B):[(A[1]+B[1])/2,(A[2]+B[2])/2]:end:
 
#Def (Mirror reflection of line l1 w.r.t. line l
MirRefLeLe:=proc(l1,l) local O,P: O:=Pt(l,l1):P:=[1,solve(subs(x=1,l1),y)]:
Le(O,MirRefPtLe(P,l)):end:
 
#Def (Mirror reflection of the origin w.r.t. to the line AB)
MirRefOf0:=proc(A,B) local q: q:=Ft([0,0],Le(A,B)): [2*q[1],2*q[2]]:end:
 
#Def (Mirror reflection of the point P w.r.t. to the line l)
MirRefPtLe:=proc(P,l) local q: 
q:=Ft([0,0],subs({x=x+P[1],y=y+P[2]},l)): [2*q[1]+P[1],2*q[2]+P[2]]:end:
 
#Def (the reflection of the point P1 w.r.t. the point P2
MirRefPtPt:=proc(P1,P2): normal([P2[1]-(P1[1]-P2[1]),P2[2]-(P1[2]-P2[2])]):end:
 
#Def(Nagel Point of the standard triangle Te(m,n))
NagelPt:=proc(m,n) local T:T:=Te(m,n):Pt(Le(T[1],PtLeCe(Le(T[2],T[3]),
Incircle(m,-1/n))),Le(T[2],PtLeCe(Le(T[1],T[3]),Incircle(-1/m,n)))):end:
 
#Def (Euler's Nine-point circle for triangle ABC)
NinePointCircle:=proc(A,B,C): Ce(MidPt(A,B),MidPt(A,C),MidPt(B,C)):end:
 
#Def(Normal to the parametric ellipse at the parametric point
NormalToEllipse:=proc(c,d,t) local P: P:=ParEllipse(c,d,t): 
diff(P[2],t)*(y-P[2])+diff(P[1],t)*(x-P[1]):end:
 
#Def (The intersection of the three perpendicular projections)
Orthocenter:=proc(A,B,C):Concurrency(Altitude(A,Le(B,C)),Altitude(B,Le(A,C)),
Altitude(C,Le(A,B))):end:
 
#OtherCeCe(C1,C2,P): The other meeting Pt of two circles C1,C2 meet at the P
OtherCeCe:=proc(C1,C2,P) if normal(subs({x=P[1],y=P[2]},C1))<>0 or 
normal(subs({x=P[1],y=P[2]},C2))<>0 then ERROR(`The circles do not meet at`, P)
: fi: MirRefPtLe(P,Le(Center(C1),Center(C2))):end:
 
#Def (Generic point on a Parametric circle center [c[1],c[2]] and radius R)
ParamCircle:=proc(c,R,t):[c[1]+R*(t+1/t)/2,c[2]+R*(t-1/t)/2/I]:end:
 
#Def (Generic point on a parametric line)
ParamLine:=proc(m,b,t):[t,m*t+b]:end:
 
#Def (Generic point on a Parametric ellipse, center [c[1],c[2]])
ParEllipse:=proc(c,d,t):[c[1]+d[1]*(t+1/t)/2,c[2]+d[2]*(t-1/t)/2/I]:end:
 
#Parametric Point on the Perpendicular Bisector of AB
ParPtPerBisect:=proc(A,B,s)local M:M:=MidPt(A,B):[M[1]+s,M[2]-s/Slope(A,B)]:end:
 
#The Pedal Triangle of the Triangle ABC w.r.t to pt P
Pedal:=proc(A,B,C,P) Ft(P,Le(A,B)),Ft(P,Le(A,C)),Ft(P,Le(B,C)): end:
 
#Def(Line through Midpoint of PQ perpendicular to PQ)
PerpMid:=proc(P,Q):PerpPQ(P,MidPt(P,Q)):end:
 
#Def(Line through Q perpendicular to PQ)
PerpPQ:=proc(P,Q):expand((y-Q[2])*(P[2]-Q[2])+(x-Q[1])*(P[1]-Q[1])):end:
 
#Def(Point between A and B that is the `p-point')
pmidpt:=proc(A,B,p): normal([A[1]+p*(B[1]-A[1]),A[2]+p*(B[2]-A[2])]):end:
 
#Def( Power of pt Pt w.r.t. circle with Center C and radius R)
Powe:=proc(C,R,Pt):DeSq(C,Pt)-R^2:end:
 
#Def (The point of intersection of lines Le1 and Le2)
Pt:=proc(Le1,Le2) local q:q:=solve(
{numer(normal(Le1)),numer(normal(Le2))},{x,y}):
[normal(simplify(subs(q,x))),normal(simplify(subs(q,y)))]:end:
 
#Def(The common point of a circle and a line that touches it)
PtLeCe:=proc(L1,C1):normal(subs(solve({L1,C1},{x,y}),[x,y])):end:
 
#Def(Quadrilateral through four lines L1,L2,L3,L4)
Quad:=proc(L1,L2,L3,L4):Pt(L1,L2),Pt(L2,L3),Pt(L3,L4),Pt(L4,L1):end:
 
#Def (the radical center of circles with centers (radiii) C1,C2,C3,R1,R2,R3
RadicalCenter:=proc(C1,R1,C2,R2,C3,R3) local C,R:
Pt(RadicalLine(C1,R1,C2,R2),RadicalLine(C1,R1,C3,R3)):end:
 
#Def( Radical line of circles with Centers C1,C2 and Radii R1, R2
RadicalLine:=proc(C1,R1,C2,R2):expand(Powe(C1,R1,[x,y])-Powe(C2,R2,[x,y])):
end:
 
#Def(The Radius  of a circle Circ)
Radius:=proc(Circ) local q:
q:=Center(Circ):radsimp(sqrt(normal(subs({x=q[1],y=q[2]},-Circ)))):end:
 
#Def (The slope of the line joining points A and B)
Slope:=proc(A,B):normal((B[2]-A[2])/(B[1]-A[1])):end:
 
#Def( Is it true that sqrt(a)+sqrt(b)=sqrt(c) ?)
Sqabc:=proc(a,b,c):ItIsZero((c-a-b)^2-4*a*b):end:

#is it true that sqrt(A)+sqrt(B)=sqrt(C)+sqrt(D)
SqRtABCD:=proc(A,B,C,D):
evalb(expand(expand(((A+B-C-D)^2-4*(A*B+C*D))^2-64*A*B*C*D))=0):
end:

 
#SSR(A,n,B): the polynomial in A[1], ..., A[n], B
#whose vanishing is equivalent to B equaling the sum 
#of the square roots of A[1],..., A[n]
SSR:=proc(A,n,B) local gu,x,i,d:if n=1 then RETURN(B^2-A[1]): fi:gu:=
expand(subs(B=B-x,SSR(A,n-1,B))):d:=degree(gu,x)/2:expand(sum(coeff(gu,x,2*i)*
A[n]^i,i=0..d)^2-A[n]*sum(coeff(gu,x,2*i+1)*A[n]^i,i=0..d)^2):end:
 
#SSR1(A,B): given a list A returns true if B is the sum
#(of one of the possibilities of sums of square roots of
#the elements of A
SSR1:=proc(A,B) local gu,i,j,mu,lu: gu:={0}:
for i from 1 to nops(A) do mu:={}: lu:=simplify(sqrt(A[i])):
for j from 1 to nops(gu) do  mu:=mu union {gu[j]+lu,gu[j]-lu}: od:gu:=mu:od:
for i from 1 to nops(gu) do if 
expand(simplify(simplify(expand(gu[i]^2-B^2),symbolic)))=
0 then
RETURN(true):fi:od:false:end:
 
#Tangent(Ce1,Pt1): Given a circle Ce1, and a point Pt1
#on it, finds the equation of the tangent
Tangent:=proc(Ce1,Pt1) local A,x0,y0: A:=coeff(Ce1,x,2):x0:=Pt1[1]: y0:=Pt1[2]:
numer(normal((y-y0)*(2*A*y0+coeff(Ce1,y,1))+(x-x0)*(2*A*x0+coeff(Ce1,x,1)))):
end:
 
#Def(Tangent to the parametric ellipse at the parametric point
TangentToEllipse:=proc(c,d,t) local P: P:=ParEllipse(c,d,t): 
diff(P[1],t)*(y-P[2])-(x-P[1])*diff(P[2],t):end:
 
#TanMt(C1,R1,m,d,R2): Intersection of common Tangents of Circle1
#with center C1 and radius R1 and Cirlce2 with center C2,distance d from C1
#such that slope(C1,C2) is tan1(b)
TanMt:=proc(C1,R1,b,d,R2) local a:
a:=d/(R2/R1-1):[C1[1]-a*cos1(b),C1[2]-a*sin1(b)]:end:
 
#Def: The condition that two circles, with given centers and radii touch
TcCesOut:=
proc(C1,R1,C2,R2):expand((R1+R2)^2-(C1[1]-C2[1])^2-(C1[2]-C2[2])^2):end:
 
#Def(Standard Triangle whose vertices are A(0,0),B(1,0) and angles
#CAB and CBA are 2*arctan(m) and 2*arctan(-n)  resp.
Te:=proc(m,n):[0,0],[1,0],Pt(y-TS(m,m)*x,y+TS(n,n)*(x-1)):end:
 
#Def(Given two circles C1,C2, decides whether they touch)
TouchCe:=proc(C1,C2) local gu: gu:=expand(subs(y=solve(C1-C2,y),C1)):
ItIsZero(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2):
end:
 
#Def(The expression whose vanishing guarantess that the symbolic
#circles touch)
TouchCe1:=proc(C1,C2) local gu: gu:=expand(subs(y=solve(C1-C2,y),C1)):
numer(normal(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2)):
end:
 
 
#Def(Given a circle C1, and a line L1, decides whether they touch)
TouchCeLe:=proc(C1,L1) local gu: gu:=expand(subs(y=solve(L1,y),C1)):
ItIsZero(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2):
end:
 
#Def(The expression whose vanishing guarantess that the symbolic
#circle C1 and Line L1 touch)
TouchCeLe1:=proc(C1,L1) local gu: gu:=expand(subs(y=solve(L1,y),C1)):
numer(normal(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2)):
end:
 
 
#Def:tan(a_1+a_2+...) expressed in terms li[1]:=tan(a_1), li[2]:=tan(a_2) ..
TS:=proc(li) local i,t:if nargs=1 then RETURN(args[1]) else
t:=TS(seq(args[i],i=2..nargs)): RETURN((args[1]+t)/(1-t*args[1])):fi:end:
 
 
###################MONTHLY PROBLEMS############################
 
#Monthly Problem Problem 10637 by C.F. Parry
P10637:=proc() local A,B,C,a,b,O1,H,alp,bet,gam,alp1,bet1,gam1,EL,m,P:
A:=[0,0]: B:=[1,0]: C:=[a,b]: O1:=Circumcenter(A,B,C):H:=Orthocenter(A,B,C):
m:=Slope(O1,H):alp:=y-A[2]-m*(x-A[1]):bet:=y-B[2]-m*(x-B[1]):
gam:=y-C[2]-m*(x-C[1]): alp1:=Billiard(alp,Le(B,C)):bet1:=Billiard(bet,Le(C,A)):
gam1:=Billiard(gam,Le(A,B)):Concurrent(alp1,bet1,gam1):P:=Concurrency
(alp1,bet1,gam1):Concurrent(alp1,bet1,gam1) and 
ItIsZero(DeSq(O1,P)-4*Circumradius(A,B,C)^2):end:
 
#Monthly Problem Problem 10673 by Mazur 
P10673:=proc()
local m,n,C,s1,s2,T,t1,t2,t3,A1,A2,A3,F1,F2,F3,P1,P2,P3,F1a,F2a,F3a:
 
T:=Te(m,n):C:=Incenter(m,n):A1:=T[1]:A2:=T[2]:A3:=T[3]:
F3:=Ft(C,Le(A1,A2)):F2:=Ft(C,Le(A1,A3)):F1:=Ft(C,Le(A2,A3)):
P1:=[A2[1]+s1*(A2[1]-A3[1]),A2[2]+s1*(A2[2]-A3[2])]:
P2:=[A1[1]+s2*(A3[1]-A1[1]),A1[2]+s2*(A3[2]-A1[2])]:
P3:=Pt(Le(Pt(Le(P1,A1),Le(P2,A2)),A3),Le(A1,A2)):
F3a:=MirRefPtLe(F3,expand(Le(C,P3))): 
F2a:=MirRefPtLe(F2,expand(Le(C,P2))): 
F1a:=MirRefPtLe(F1,expand(Le(C,P1))): 
t1:=Le(P1,F1a):t2:=Le(P2,F2a):t3:=Le(P3,F3a):
Colinear(Pt(t1,Le(P2,P3)),Pt(t2,Le(P3,P1)),Pt(t3,Le(P1,P2))):
end:
 
#Monthly Problem P10678, Aug./Sep. 1998, proposed by Clark 
#Kimberling and Peter Yff
P10678:=proc() local m,n,T,Ce1,A1,A2,A3,B1,B2,B3: 
T:=Te(m,n): Ce1:=Incircle(m,n):A1:=T[1]:A2:=T[2]:A3:=T[3]:
B3:=Kiss(A1,A2,Ce1):B2:=Kiss(A1,A3,Ce1):B1:=Kiss(A2,A3,Ce1):
Concurrent(Le(A1,B1),Le(A2,B2),Le(A3,B3)): end:
 
sin1:=proc(a):(a-1/a)/I/2:end:cos1:=proc(a):(a+1/a)/2:end:
tan1:=proc(a):sin1(a)/cos1(a):end:
#Monthly Problem P10693, Nov. 1998,  proposed by Wu Wei Chao
P10693:=proc() local  a,b,c, AB,BP,Q,R,D,PC,D1,Q1,R1:
AB:=sin1(b^2)/sin1(a^2*b^2):BP:=sin1(a^2*c^2)*AB/sin1(c^2):PC:=1-BP:
D:=[Incenter(tan1(a),tan1(b))[1],0]:Q:=Incenter(tan1(a),tan1(c)):
Q:=[BP*Q[1],BP*Q[2]]:R:=Incenter(1/tan1(c),tan1(b)):R:=[BP+PC*R[1],PC*R[2]]:
D1:=[Incenter(-1/tan1(a),-1/tan1(b))[1],0]:Q1:=Incenter(-1/tan1(a),-1/tan1(c)):
Q1:=[BP*Q1[1],BP*Q1[2]]:R1:=Incenter(-tan1(c),-1/tan1(b)):
R1:=[BP+PC*R1[1],PC*R1[2]]:evalb(normal(Slope(R,D)*Slope(Q,D))=-1 and 
nops(normal({DeSq(Q,D)/DeSq(R1,D1),DeSq(D,R)/DeSq(D1,Q1),
DeSq(R,Q)/DeSq(Q1,R1)}))=1 and Concurrent(y,Le(Q,R),Le(Q1,R1))):
end:
 
#Monthly Problem P10703, Dec. 1998,  proposed by Jean Anglesio
P10703:=proc() local m,n,T,I1,C1,O1,H1,W1,G1,N1,S1,T1,U1,V1:
T:=Te(m,n):I1:=Incenter(m,n):C1:=Centroid(T):O1:=Circumcenter(T):
H1:=Orthocenter(T):W1:=Center(NinePointCircle(T)):G1:=GergonnePt(m,n):
N1:=NagelPt(m,n):S1:=Pt(Le(I1,G1),Le(O1,C1)):T1:=Pt(Le(I1,G1),Le(O1,N1)):
U1:=Pt(Le(I1,G1),Le(W1,N1)):V1:=Pt(Le(I1,G1),Le(H1,N1)):
[ItIsZero(normal(DeSq(C1,H1)/DeSq(H1,S1)-1/9)),
[ItIsZero(normal(DeSq(S1,T1)/DeSq(S1,I1)-(10/15)^2)),
ItIsZero(normal(DeSq(S1,T1)/DeSq(S1,U1)-(10/18)^2)),
ItIsZero(normal(DeSq(S1,T1)/DeSq(S1,V1)-(10/30)^2))],
[ItIsZero(normal(DeSq(N1,O1)/DeSq(T1,O1)-(3/1)^2)),
ItIsZero(normal(DeSq(N1,W1)/DeSq(U1,W1)-(5/3)^2)),
ItIsZero(normal(DeSq(N1,H1)/DeSq(V1,H1)-1))]]:end:
 
#Monthly Problem P10710, Jan. 1999,  proposed by Bogdan Suceava
P10710:=proc() local m,n,T,A,B,C,D,E,F,I1,M,N,P,Q:T:=Te(m,n):A:=T[1]: B:=T[2]: 
C:=T[3]:I1:=Incenter(m,n):D:=Ft(I1,Le(B,C)):E:=Ft(I1,Le(A,C)):
F:=Ft(I1,Le(A,B)):
M:=Pt((y-A[1])-Slope(B,C)*(x-A[2]),Le(D,E)):N:=Pt((y-A[1])-Slope(B,C)*(x-A[2]),
Le(D,F)):P:=MidPt(D,M):Q:=MidPt(D,N):Concyclic(A,E,F,I1,P,Q):end:
 
#Monthly Problem 10734, proposed by Floor van Lamoen, May 1999
P10734:=proc() local m,n,T,SL,A,B,C,H,I1,O,AB,AC,BC: T:=Te(m,n):A:=T[1]: 
B:=T[2]: C:=T[3]: AB:=sqrt(DeSq(A,B)):AC:=-simplify(sqrt(DeSq(A,C)),symbolic):
BC:=-simplify(sqrt(DeSq(B,C)),symbolic): H:=Orthocenter(T):I1:=Incenter(m,n): 
O:=Circumcenter(T): evalb(RadicalCenter(A,AC+AB,B,AB+BC,C,BC+AC)=
MirRefPtPt(MirRefPtPt(H,O),I1)):end:
 
#Monthly Problem 10749, proposed by Alain Grigis, Aug.-Sep. 1999
P10749:=proc() local A,B,C,p,P,Q,R,S,X,p0:
B:=[0,0]: A:=[sqrt(3),0]: C:=[0,1]: P:=[0,p]:
Q:=Pt(Billiard(Le(A,P),Le(B,C)),Le(A,C)):
R:=Pt(Billiard(Le(P,Q),Le(A,C)),Le(A,B)):
S:=Pt(Billiard(Le(Q,R),Le(A,B)),Le(A,C)):
p0:=solve(normal(subs({x=0,y=0},Billiard(Le(R,S),Le(A,C)))/p),p):
P:=subs(p=p0,P):Q:=subs(p=p0,Q):R:=subs(p=p0,R):S:=subs(p=p0,S):
X:=Concurrency(Le(A,P),Le(Q,R),Le(S,B) ):
evalb(
Concurrent(Le(A,P),Le(Q,R),Le(S,B)) and
Slope(B,X)=sqrt(3)/2 and Slope(X,S)=sqrt(3)/2 and
simplify(De(A,X)-De(X,P)-De(P,Q)-De(Q,X))=0 and 
simplify(De(A,X)-De(X,R)-De(R,S)-De(S,X))=0 and
simplify(De(A,X)-2*De(X,B))=0) 
end:

# P10780a(m,n,r,Base): Proves that 
# The radius of the partner of the circle
# of radius r touching the sides CA and AB in the triangle
# ABC where length(AB)=Base, and angle CAB=2*arctan(m)
# and angle ABC=2*arctan(n) equals
# R:=(-n/m)*r+(n/(1-n*m))*Base: 
P10780a:=proc()
local m,n,r,P1,P2,C,Cir1,Cir2,Li,gu1,gu2,m1,R: 
R:=(-n/m)*r+n/(1-n*m):  P1:=[r/m,r]: P2:=[1-R/n, R]:C:=Te(m,n)[3]: 
Li:=(y-C[2])-(x-C[1])*m1:
Cir1:=expand((x-P1[1])^2+(y-P1[2])^2-P1[2]^2):
Cir2:=expand((x-P2[1])^2+(y-P2[2])^2-P2[2]^2):
evalb(solve(TouchCeLe1(Cir1,Li)/(m1-TS(m,m)),m1)=
      solve(TouchCeLe1(Cir2,Li)/(m1-TS(-n,-n)),m1));
end:
 
#Monthly Problem 10780*, proposed by Kiran Kedlaya, Jan. 2000
P10780:=proc() local f,m,n,k,r,T,BC,CA,lu:
print(`This solution is dedicated to the memory of Rodica Simion`):
lprint(``):
lprint(``):
#The line below is verified by P10780a();
f:=(m,n,r,C)->normal((-n/m)*r+(n/(1-n*m))*C): 
T:=Te(m,n): k:=1/TS(m,n):
BC:=sqrt(factor(DeSq(T[2],T[3]))):CA:=sqrt(factor(DeSq(T[3],T[1]))):
lu:=f(m,n,r,1);lu:=f(n,k,lu,BC);lu:=f(k,m,lu,CA);lu:=f(m,n,lu,1);
lu:=f(n,k,lu,BC);lu:=f(k,m,lu,CA);evalb(lu=r):end:
 

#Monthly Problem 10783, proposed by Wu Wei Chao, Feb. 2000
P10783:=proc() local t2,t3,t4,A,B,C,D,E,F,G,H,m,n:
A:=ParamCircle([0,0],1,1):B:=ParamCircle([0,0],1,t2):
C:=ParamCircle([0,0],1,t3):D:=ParamCircle([0,0],1,t4):
E:=[m*C[1]+(1-m)*D[1],m*C[2]+(1-m)*D[2]]:
F:=[n*C[1]+(1-n)*D[1],n*C[2]+(1-n)*D[2]]:
G:=Circumcenter(B,C,E):H:=Circumcenter(A,D,F):
F:=subs(n=solve(AREA(Pt(Le(A,B),Le(C,D)),G,H),n),F):
evalb(Ce(A,B,E)=Ce(A,B,F)):end:

#Monthly Problem 10796, proposed by Floor van Lamoen, April 1999
P10796:=proc() local A,B,C,D,A1,B1,C1: A:=[0,0]:B:=[1,0]:
A1:=Ft(A,Le(B,C)):B1:=Ft(B,Le(A,C)):C1:=Ft(C,Le(A,B)):
D:=Concurrency(EulerLine(A,B1,C1),EulerLine(A1,B,C1),EulerLine(A1,B1,C)):
ItIsZero(subs({x=D[1],y=D[2]},NinePointCircle(A,B,C))):
end:

#Monthly Problem 10804, proposed by Achilleas Sinefakopoulos, May 2000
P10804:=proc() local A,B,C,D,t,L,P,E,F,i,lu1,lu2:
for i from 1 to 4 do P[i]:=ParEllipse([0,0],[1,1],t[i]):
L[i]:=TangentToEllipse([0,0],[1,1],t[i]):od:
A:=Pt(L[1],L[2]):B:=Pt(L[2],L[3]):
C:=Pt(L[3],L[4]):D:=Pt(L[4],L[1]): E:=P[2]:F:=P[4]: 
lu1:=factor(numer(normal(Ce(A,B,C)-Ce(A,B,D)))):
lu2:=factor(numer(normal(DeSq(A,E)/DeSq(E,B)-DeSq(D,F)/DeSq(F,C)))):
evalb({solve(lu1,t[3])} intersect {solve(lu2,t[3])} minus {t[1]}<>{}):end:

#Monthly Problem 10810 (June-July 2000), proposed by J.-B. Romero Marquez
P10810:=proc()local A,B,C,D,JB:
JB:=proc(A,B,C,D) local A1,B1:
A1:=Pt((y-B[2])-Slope(C,D)*(x-B[1]),Le(A,D)):
B1:=Pt((y-A[2])-Slope(D,C)*(x-A[1]),Le(B,C)):
Pt(Le(A,B),Le(A1,B1)): end:
A:=[0,0]: B:=[1,0]: 
evalb(Slope(JB(A,B,C,D),JB(B,C,D,A))=Slope(JB(C,D,A,B),JB(D,A,B,C))):
end:

#Monthly Problem 10845, Jan. 2001,proposed by Ciprian Demeter
P10845:=proc() local A,B,C,a,b,c,T,T1,IntBisA,ExtBisA,m,n,E,F,G:
m:=TS(a,c): n:=TS(b,c):T:=Te(m,n):T1:=Te(a,b):
B:=T[1]:  A:=T[2]:C:=T[3]:E:=T1[2]:
IntBisA:=y-A[2]-expand((x-A[1])*TS(m,1/n)):
ExtBisA:=x-A[1]+expand((y-A[2])*TS(m,1/n)):
F:=Ft(E,IntBisA):G:=Ft(E,ExtBisA):
Colinear(F,G,MidPt(B,C)):
end:

#Montly Problem 10874, May 2001, proposed by Wu Wei Chao
P10874:=proc() local a,b,c,d,A,B,C,D1,P,U,V:
A:=ParEllipse([0,0],[1,1],a): B:=ParEllipse([0,0],[1,1],b):
C:=ParEllipse([0,0],[1,1],c):D1:=ParEllipse([0,0],[1,1],d):
P:=Pt(Le(A,C),Le(B,D1)):U:=Circumcenter(A,P,B):V:=Circumcenter(C,P,D1):
evalb(Slope([0,0],U)=Slope(P,V) and Slope([0,0],V)=Slope(U,P)),
factor(AREA([0,0],U,V))=0:
end:

#Montly Problem 11554, Feb. 2011, proposed by Zhang Yun
P11554:=proc() local T,I1,m,n:
T:=Te(m,n): I1:=Incenter(m,n):
Concurrent(
Le(MirRefPtLe(I1,Le(T[2],T[3])),T[1]),
Le(MirRefPtLe(I1,Le(T[1],T[3])),T[2]),
Le(MirRefPtLe(I1,Le(T[1],T[2])),T[3])
):
end:


############END OF MONTHLY PROBLEMS#####################################
 
 
#############IMO PROBLEMS##############################
I78_4:=proc() local m,T,B,C,A,D,P,Q,Ce1,Ce2,t,lu,M,J,i: T:=Te(m,m):B:=T[1]:
C:=T[2]:A:=T[3]:P:=[B[1]+t*(A[1]-B[1]),B[2]+t*(A[2]-B[2])]:
Q:=[C[1]+t*(A[1]-C[1]),B[2]+t*(A[2]-C[2])]:D:=Pt(PerpPQ(A,P),PerpPQ(A,Q)):
J:=Incenter(m,m):Ce1:=Ce(A,B,C):Ce2:=expand((x-D[1])^2+(y-D[2])^2-DeSq(D,P)):
lu:={solve(TouchCe1(Ce1,Ce2),t)}: M:=MidPt(P,Q):
member(J,{seq(normal(subs(t=lu[i],M)),i=1..nops(lu))}):end:
 
I79_3:=proc() local t,P,Q,lu,t1,t2: P:=t->[cos(t),sin(t)]:
Q:=proc(t):evalc(1-R*exp(-t0*I)+R*exp(I*(t-t0))):[coeff(",I,0),coeff(",I,1)]:
end:evalb(diff(Pt(PerpMid(P(t1),Q(t1)),PerpMid(P(t2),Q(t2))),t1)=0):end:
 
I82_2:=proc() local m,n,T,A1,A2,A3,D,M1,M2,M3,T1,T2,T3,S1,S2,S3: 
T:=Te(m,n): A1:=T[1]:A2:=T[2]:A3:=T[3]:
D:=Incenter(m,n):M1:=MidPt(A2,A3):M2:=MidPt(A1,A3):M3:=MidPt(A1,A2):
T1:=Ft(D,Le(A2,A3)):T2:=Ft(D,Le(A1,A3)):T3:=Ft(D,Le(A1,A2)):
S1:=MirRefPtLe(T1,y-m*x):S2:=MirRefPtLe(T2,y+n*x-n):
S3:=MirRefPtLe(T3,y-A3[2]-expand((x-A3[1])*TS(m,1/n))):
Concurrent(Le(M1,S1),Le(M2,S2),Le(M3,S3)):end:
 
 
I82_5:=proc() local A,B,C,D,E,F,P,i,gu,M,N,r:
for i from 0 to 5 do gu:=evalc(exp(i*2*Pi*I/6)):
P[i]:=[coeff(gu,I,0),coeff(gu,I,1)]: od:
A:=P[0]:B:=P[1]:C:=P[2]:D:=P[3]:E:=P[4]:F:=P[5]:
M:=[A[1]+r*(C[1]-A[1]),A[2]+r*(C[2]-A[2])]:
N:=[C[1]+r*(E[1]-C[1]),C[2]+r*(E[2]-C[2])]:solve(AREA(B,M,N),r):end:
 
#######################END####################
 
 
#####Ancestors
##Fathers of Theorems
ABBA[AreaFormula]:={ItIsZero,DeSq,AREA}:
ABBA[Bretschneider]:={ItIsZero,DeSq,AREA}:
ABBA[Brianchon]:={ TangentToEllipse,Pt,Concurrent,Le}:
ABBA[Butterfly]:={ParamCircle,Pt,Le,PerpPQ,DeSq,ItIsZero}:
ABBA[Carnot]:={Te,SSR1,Circumcenter,Ft,Le,ItIsZero,DeSq,Circumradius,Inradius}:
ABBA[Casey]:={ParamCircle,ComTangLgtSq,ItIsZero}:
ABBA[CentroidExists]:={Concurrent,Le,MidPt,Le}:
ABBA[Ceva]:={Pt,Le,ItIsZero,DeSq}:
ABBA[Clifford]:={OtherCeCe}:
ABBA[deLongchamps]:={Circumcenter,Orthocenter,EulerLine,ItIsZero}:
ABBA[Desargues]:={ParamLine,Colinear,Pt,Le}:
ABBA[EightPointCircleExists]:={MidPt,Concyclic,Ft,Le}:
ABBA[EulerLineExists]:={Colinear,Orthocenter,Circumcenter,Centroid}:
ABBA[EulerTetrahedronVolumeFormula]:={DeSqG,AREA}:
ABBA[EulerTriangleFormula]:=
{Te,Incenter,Circumcenter,Inradius,Circumradius,DeSq,ItIsZero}:
ABBA[Feuerbach]:={TouchCe,NinePointCircle,Te,Incircle}:
ABBA[FeuerbachConic]:={NinePointCircle,Te,Orthocenter,ItIsZero}:
ABBA[FinslerHadwiger]:={Pt,MidPt,Le,ItIsZero,DeSq,Slope}:
ABBA[FoxTalbot]:={Quad,Le,MidPt,Concurrent}:
ABBA[Fregier]:={ParEllipse,NormalToEllipse}:
ABBA[Fuhrmann]:={SSR1,ParamCircle,DeSq,ItIsZero}:
ABBA[Gergonne]:={Te,Incircle,Concurrent,Le,PtLeCe}:
ABBA[Griffiths]:={Circumcenter,Ce,Pedal,NinePointCircle}:
ABBA[Herron]:={DeSq,ItIsZero,AREA}:
ABBA[Hoehn]:={DeSq,Le,Pt,ItIsZero}:
ABBA[IncenterExists]:={Concurrent,TS}:
ABBA[Johnson]:={ParamCircle,MirRefOf0,ItIsZero,Radius,Ce}:
ABBA[Lehmus]:={Pt,TS,DeSq}:
ABBA[Lemoine]:={Te,Centroid,Concurrent,MirRefLeLe,Le}:
ABBA[LeonAnne]:={Le,MidPt,AREA,ItIsZero}:
ABBA[MarionMorgan]:={pmidpt,Le,Pt,AREA,ItIsZero}:
ABBA[MedianTriangleLocus]:={AntiMedial,Te,Pedal,Incenter,DeSq,MidPt,Colinear}:
ABBA[Menelaus]:={Pt,Le,ItIsZero,DeSq}:
ABBA[Miquel]:={ParamCircle,ParPtPerBisect,MirRefPtLe,Concyclic}:
ABBA[Monge]:={sin1,cos1,Colinear,TanMt}:
ABBA[Morley]:={Pt,TS,ItIsEqui}:
ABBA[Nagel]:={Te,Incircle,Concurrent,Le,PtLeCe}:
ABBA[Napoleon]:={ItIsEqui,CET}:
ABBA[NinePointCircleExists]:={Ft,Le,MidPt,Orthocenter,Concyclic}:
ABBA[Nobbs]:={Contact,Colinear,Pt,Le}: 
ABBA[OrthocenterExists]:={Concurrent,Altitude,Le}:
ABBA[Pappus]:={ParamLine,Colinear,Pt,Le}:
ABBA[Pascal]:={ParEllipse,Colinear,Pt,Le}:
ABBA[Pivot]:={Ce,OtherCeCe}:
ABBA[Poncelet]:={TangentToEllipse,Pt,Circumradius,Circumcenter,ParamCircle,
TouchCeLe1,TouchCeLe}:
ABBA[Ptolemy]:={ParamCircle,Sqabc,DeSq}:
ABBA[Purser]:={ParamCircle,DeSq,SSR}:
ABBA[RadicalCenterExists]:={Concurrent, RadicalLine}:
ABBA[Sadov]:={DeSq,ParamCircle,SqRtABCD}:
ABBA[Simson]:={ParamCircle,Colinear,Ft,Le}:
ABBA[Soddy]:={TcCesOut,ItIsZero}:
ABBA[Varignon]:={MidPt,ItIsZero,Slope}:
ABBA[Viviani]:={SSR,Te,ItIsZero,DeSq,Ft,Le}:
ABBA[vonAubel]:={MDOS,ItIsZero,Slope,DeSq}:
ABBA[Wittenbauer]:={Pt,Le,CentroidQ}:
##End of Fathers of Theorems
 
##Fathers of Definitions
 
ABBA[Altitude]:={}:
ABBA[AntiMedial]:={}:
ABBA[AREA]:={}:
ABBA[Billard]:={BilliardSym}:
ABBA[BillardSym]:={Pt,Sym}:
ABBA[Ce]:={}:
ABBA[Center]:={}:
ABBA[Centroid]:={Concurrency,Le,MidPt}:
ABBA[CentroidQ]:={AREA,Centroid}:
ABBA[CET]:={Circumcenter}:
ABBA[Circumcenter]:={Center,Ce}:
ABBA[Circumradius]:={Radius,Ce}:
ABBA[Colinear]:={AREA}:
ABBA[ComTangLgtSq]:={DeSq}:
ABBA[Concyclic]:={Ce}:
ABBA[Concurrency]:={}:
ABBA[Concurrent]:={}:
ABBA[Contact]:={Te,Incenter,Ft,Le}:
ABBA[De]:={DeSq}:
ABBA[DePtLeSq]:={DeSq,Pt,Altitude}:
ABBA[DeSq]:={}:
ABBA[DeSqG]:={}:
ABBA[Excircles]:={Te,Incircle,TouchCeLe,Le}:
ABBA[EulerLine]:={Le,Orthocenter,Circumcenter}:
ABBA[Ft]:={Pt,Altitude}:
ABBA[GergonnePt]:={Te,Incircle,Pt,Le,PtLeCe}:
ABBA[Incenter]:={Te,Concurrency,TS}:
ABBA[Incircle]:={Inradius,Incenter}:
ABBA[Inradius]:={Te,Incenter,DePtLeSq,Le,DePtLeSq}:
ABBA[ItIsEqui]:={DeSq}:
ABBA[ItIsZero]:={}:
ABBA[Kiss]:={Tangent,Colinear}:
ABBA[Le]:={AREA}:
ABBA[MDOS]:={Pt,Le}:
ABBA[MidPt]:={}:
ABBA[MirRefLeLe]:={Pt,Le,MirRefPtLe}:
ABBA[MirRefPtLe]:={Ft,Le}:
ABBA[MirRefOf0]:={Ft,Le}:
ABBA[NagelPt]:={Te,Incircle,Pt,Le,PtLeCe}:
ABBA[NinePointCircle]:={Ce,MidPt}:
ABBA[NormalToEllipse]:={ParEllipse}:
ABBA[Orthocenter]:={Concurrency,Altitude,Le}:
ABBA[OtherCeCe]:={}:
ABBA[ParamCircle]:={}:
ABBA[ParamLine]:={}:
ABBA[ParEllipse]:={}:
ABBA[ParPtPerBisect]:={MidPt,Slope}:
ABBA[Pedal]:={Ft,Le}:
ABBA[PerpMid]:={PerpPQ,MidPt}:
ABBA[PerpPQ]:={}:
ABBA[pmidpt]:={}:
ABBA[Powe]:={DeSq}:
ABBA[Pt]:={}:
ABBA[PtLeCe]:={}:
ABBA[Quad]:={Pt}:
ABBA[RadicalLine]:={Powe}:
ABBA[Radius]:={Center}:
ABBA[sin1]:={}:
ABBA[cos1]:={}:
ABBA[tan1]:={sin1,cos1}:
ABBA[Slope]:={}:
ABBA[Sqabc]:={ItIsZero}:
ABBA[SqRtABCD]:={}:
ABBA[SSR]:={}:
ABBA[Te]:={Pt,TS}:
ABBA[TS]:={}:
ABBA[Tangent]:={}:
ABBA[TangentToEllipse]:={ParEllipse}:
ABBA[TanMt]:={sin1,cos1}:
ABBA[Thebault]:={Incenter,TouchCe1,TouchCeLe1,Le,Colinear}:
ABBA[TouchCe]:={ItIsZero}:
ABBA[TouchCe1]:={}:
ABBA[TouchCeLe]:={ItIsZero}:
ABBA[TouchCeLe1]:={}:
ABBA[TcCesOut]:={}:
##End of Fathers of Definitions
 
#IterAbba(Set1): Given a set of definitions
#joins to them the definitions that depend on
#them
IterAbba:=proc(Set1)
local i,gu:
gu:={}:
for i from 1 to nops(Set1) do
gu:=gu union ABBA[op(i,Set1)]:
od:
gu union Set1:
end:
 
 
#ANCESTORS(Set1): the set of all ancestors of the
#definitions in the set Set1, including themselves
ANCESTORS:=proc(Set1)
local gu,mu,mun:
gu:=Set1:
mu:=IterAbba(gu):
 
while mu<>gu do
mun:=IterAbba(mu):
gu:=mu:
mu:=mun:
od:
 
mu:
end:
 
#SelfContained(Theorem): given a theorem, prints its
#statment, plus all the required definitions
SelfContained:=proc(Theorem1)
local gu,i,t0:
gu:=ABBA[Theorem1]:
gu:=ANCESTORS(gu):
lprint(``):
lprint(`The definitions needed for the`,Theorem1,`Theorem are `):
print(``):
for i from 1 to nops(gu) do
lprint(gu[i],`:=`):
print(gu[i]):
od:
 
lprint(`The statement of the`,Theorem1, `  Theorem is `):
print(``):
print(Theorem1):
print(``):
lprint(`Now let Maple prove it; The theorem is`):
t0:=time():
print(Theorem1());
print(``):
lprint(`The whole proof took`, time() -t0, ` seconds of CPU time `):
end:

#Contributed by Matthew Russell (Amer. Math. Monthly Problem #11615, Feb. 2012)
P11615:=proc() local T,m,n,A,B,C,D,E,F,K,M,N,P,MK,NK,PK,MN,MP,NP,SAK,SBK,SCK,ParD,ParE,ParF:
print(`Contributed by Matthew Russell (Amer. Math. Monthly Problem #11615, Feb. 2012)`):
T:=Te(m,n):
A:=T[1]:
B:=T[2]:
C:=T[3]:
K:=[K1,K2]:
M:=MidPt(B,C):
N:=MidPt(A,C):
P:=MidPt(A,B):
MK:=Le(M,K):
NK:=Le(N,K):
PK:=Le(P,K):
MN:=Le(M,N):
MP:=Le(M,P):
NP:=Le(N,P):
D:=Pt(MK,NP):
E:=Pt(NK,MP):
F:=Pt(PK,MN):
SAK:=Slope(A,K):
SBK:=Slope(B,K):
SCK:=Slope(C,K):
ParD:=LePtSlope(D,SAK):
ParE:=LePtSlope(E,SBK):
ParF:=LePtSlope(F,SCK):

evalb(Concurrent(ParD,ParE,ParF)
or evalb(subs(x=K[1],y=K[2],Le(A,B))=0)
or evalb(subs(x=K[1],y=K[2],Le(A,C))=0)
or evalb(subs(x=K[1],y=K[2],Le(B,C))=0)):

end:

LePtSlope:=proc(P,m):
expand((y-P[2])-m*(x-P[1])):
end:





Ekhad:=proc() local i,P,s,t: 

for i from 1 to 4 do 
 P[i]:=[s[i],t[i]]:
od:


Colinear(
Pt(Le(P[1],P[2]),Le(Pt(Le(P[1],P[3]), Le(P[2],P[4])), Pt(Le(P[1],P[4]), Le(P[2],P[3])))),
Pt(Le(P[1],P[3]),Le(Pt(Le(P[1],P[2]), Le(P[3],P[4])), Pt(Le(P[1],P[4]), Le(P[2],P[3])))),
Pt(Le(P[2],P[3]),Le(Pt(Le(P[1],P[2]), Le(P[3],P[4])), Pt(Le(P[1],P[3]), Le(P[2],P[4]))))):
end:

# Pt1:={{1, 2}, {{{1, 3}, {2, 4}}, {{1, 4}, {2, 3}}}}, 
#Pt2:={{1, 3}, {{{1, 2}, {3, 4}}, {{1, 4}, {2, 3}}}}, 
#Pt3:={{2, 3}, {{{1, 2}, {3, 4}}, {{1, 3}, {2, 4}}}}



#P12027():Amer. Math. Monthly Problem #12027, March 2018)
P12027:=proc() local m,n,T,Ci,A1,B1,C1,r,R,D1,E1,F1,X1,Y1,Z1,gu,lu,lu1,i:
T:=Te(m,n):
Ci:=Incircle(m,n):
r:=Inradius(m,n):
R:=Circumradius(T):

if subs({m=1/3,n=1/4},r)<0 then
 r:=-r:
fi:

if subs({m=1/3,n=1/4},R)<0 then
 R:=-R:
fi:

A1:=T[1]: B1:=T[2]: C1:=T[3]:

D1:=PtLeCe(Le(B1,C1),Ci):
E1:=PtLeCe(Le(C1,A1),Ci):
F1:=PtLeCe(Le(A1,B1),Ci):


gu:=[solve({Le(A1,D1),Ci},{x,y})]:

gu:=normal({subs(gu[1],[x,y]),subs(gu[2],[x,y])}) minus {D1}:


X1:=gu[1]:
gu:=[solve({Le(B1,E1),Ci},{x,y})]:
gu:=normal({subs(gu[1],[x,y]),subs(gu[2],[x,y])}) minus {E1}:
Y1:=gu[1]:


gu:=[solve({Le(C1,F1),Ci},{x,y})]:
gu:=normal({subs(gu[1],[x,y]),subs(gu[2],[x,y])}) minus {F1}:

Z1:=gu[1]:


lu:=
[simplify(sqrt(DeSq(A1,X1)/DeSq(X1,D1)),symbolic),
simplify(sqrt(DeSq(B1,Y1)/DeSq(Y1,E1)),symbolic),
simplify (sqrt(DeSq(C1,Z1)/DeSq(Z1,F1)) ,symbolic)]:

lu1:=[]:

for i from 1 to nops(lu) do
if subs({m=1/3,n=1/4},lu[i])<0 then
 lu1:=[op(lu1),-lu[i]]:
 else
 lu1:=[op(lu1),lu[i]]:
fi:
od:

lu:=lu1:
evalb(normal(convert(lu,`+`)-(R/r-1/2))=0);


end:





MiquelFiveCircle:=proc() local s,P,Q,Qa,gu,i,r,C:
s[5]:=-1/mul(s[i],i=1..4):
gu:=1:

for i from 1 to 5 do
P[i]:=ParamCircle([0,0],1,gu):
Q[i]:=ParamCircle([0,0],1,gu*s[i]):
r[i]:=expand(DeSq(P[i],Q[i])):
C[i]:=expand(DeSq([x,y],P[i])-r[i]):
gu:=gu*s[i]*s[i+1]:
od:

for i from 1 to 4 do
 Qa[i]:=OtherCeCe(C[i],C[i+1],Q[i]):
od:

evalb(normal(DeSq(Pt(Le(Qa[1],Qa[2]),Le(Qa[3],Qa[4])),P[3])-DeSq(Q[2],P[3]))=0):
end: