supressbanner =	False;
quick =			False;
showAllSteps =	False;

h[x_]:= 2K/x;

csum[expr_]:=
	expr + (expr/.{a->b,b->c,c->a,A->B,B->C,C->A}) +
	       (expr/.{a->c,b->a,c->b,A->C,B->A,C->B});

cprod[expr_]:=
	expr * (expr/.{a->b,b->c,c->a,A->B,B->C,C->A}) *
	       (expr/.{a->c,b->a,c->b,A->C,B->A,C->B});

cvec[expr_]:=
	{expr, (expr/.{a->b,b->c,c->a,A->B,B->C,C->A}),
	       (expr/.{a->c,b->a,c->b,A->C,B->A,C->B})};

triangcount =	0;
triangtrue =	0;

trineq[ex_]:=
Block[{varlist,sub,result,left,right,op,pr,temp,expr},

 expr = ex;
 If[showproof,showreason = True];
 
 If[expr===True || expr===False,Return[expr]];

 op =		getop[expr];
 normalorder[];

 If[!supressbanner,
 	Print[" "];
 	Print["To prove: ",op[left,right]];
	triangcount++;
   ];

 varlist =	Variables[expr];

 If[MemberQ[varlist,A],handleTrig[]];

 varlist =	Variables[op[left,right]];

(*
 result = checkobvious[];
 If[result==True || result==False,Return[result]];
*)

 sub = False;

 substituteq[r->K/s];
 substituteq[R->a*b*c/(4K)];

 If[sub && showproof,
    Print["We get:"];
	Print[op[left,right]];	(* do not expand *)
							(* should we simplify? *)
   ];

 triclearfractions[];

 result = trigcdize[];
 If[result===True || result===False,
 	If[result && !supressbanner, triangtrue++];
	Return[result];
   ];

 result = checkobvious[];
 If[result==True || result==False,Return[result]];

 varlist =	Variables[op[left,right]];
 handleK[];

 sub = False;
 substituteq[F->Sqrt[s*(s-a)*(s-b)*(s-c)]];
 substituteq[s->(a+b+c)/2];
 If[sub && showproof,
    Print["We get:"];
	Print[op[left,right]];	(* do not expand *)
   ];
 triclearfractions[];
 collect[];

 result = trigcdize[];

 left =	Together[left];
 right =Together[right];
 expr =	op[left,right];
 If[result===True || result===False,
 	If[result && !supressbanner, triangtrue++];
	Return[result];
   ];
 expr =	(expr/.{a->(y+z)/2,b->(z+x)/2,c->(x+y)/2});
 expr =	Together[expr];

 If[showproof,
   Print["Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get:"];
   Print[expr];		(* do not expand *)
   ];

 left =		Part[expr,1];
 right =	Part[expr,2];

 triclearfractions[];

 expr =		op[left,right];
 result =	homogineq[expr,{x,y,z}];

 If[result && !supressbanner, triangtrue++];

 Return[result];

 ];

isolateK[] :=
Block[{co,saveshowproof,savebanner,saveshowreason,
	other,side,oldleft,temp},

(* left, right, op are implicit arguments. *)

    (* Bring terms with K to the left side. *)

    oldleft =	left;
    left =	Collect[left,K];
    right =	Collect[right,K];
    temp =	Coefficient[left,K,0];
    left =	left - temp;
    right =	right - temp;
    temp =	Coefficient[right,K,1];
    left =	left - temp*K;
    right =	right - temp*K;

    (* See if the coefficient of K is negative. *)

    co =			Coefficient[left,K];
    other =			right;
    saveshowproof =	showproof;
    saveshowreason =showreason;
    savebanner =	supressbanner;
    showproof = 	False;
    showreason =	False;
    supressbanner =	True;
    side =			"left";

    (*  If the coefficient of K is negative, then swap
	the two sides of the inequality, that is, change a<b
	into (-b) < (-a) .
    *)

    If[trineq[co<0]===True,
		temp =	-left;
		left =	-right;
		right =	temp;
		other =	-other;
		side =	"right";
		co =	-co;
	(* else *),
		If[!quick && trineq[co>0]=!=True,
			Print["Cannot determine sign of:",co];
			showproof =		saveshowproof;
			showreason =	saveshowreason;
			supressbanner =	savebanner;
			Return[notyetimplemented];
		  ];
	  ];

    If[!quick && trineq[other>0]=!=True,
		Print["Warning: cannot determine if the other side,"];
		Print[other];
		Print["is positive. (Assuming it is.)"];
	  ];

    showproof =		saveshowproof;
    showreason =	saveshowreason;
    supressbanner =	savebanner;

    If[showproof,
    	If[Together[oldleft-left]=!=0,
			Print["Bringing all terms involving K to the ",
				side," side yields:"];
	  		Print[op[left,right]];
		  ];

    	If[!quick,
			Print["Since ",co," is positive, and since"];
			Print[other," is positive,"];
    	  ];
		Print["we can square both sides to get:"];
      ];

  ];

substituteq[eq_]:=
 (* eq is if the form "var->replacement" *)

 (* Implicit inputs: left, right, op, showproof *)
 (* Implicit outputs: sub is set TRUE if var occurs
 	in either left or right. *)

Block[{var,varlist},

 var =		First[eq];
 varlist =	Variables[op[left,right]];

 If[MemberQ[varlist,var],
    If[showproof,
		Print["Let ",Part[eq,1],"=",InputForm[Part[eq,2]],"."];
	  ];
	left =	(Collect[left,var]/.eq);
	right =	(Collect[right,var]/.eq);
	(*
	   left:	expand(ratsimp(left)),
	   right:	expand(ratsimp(right)),
	*)
	sub = True;
   ];

  ];

handleK[]:=
 (* Implicit arguments are left, right, op, showproof. *)
Block[{area},

 area =	Sqrt[s*(s-a)*(s-b)*(s-c)];

 handleK2[];

 trigcdize[];

 varlist =	Variables[op[left,right]];

 If[MemberQ[varlist,K],
	isolateK[];

    (* Square both sides. *)

    left =	left/.{K->area};
    left =	left^2;
    right =	right/.{K->area};
    right =	right^2;
    left =	Simplify[left];
    right =	Simplify[right];

    If[showproof,
    	Print[op[left,right]];	 (* could expand if desired *)
      ];

    triclearfractions[];
    collect[];
    trigcdize[];

   ];

 ];

handleK2[]:=
Block[{},

 left =		Expand[left];
 right =	Expand[right];

 oldleft =	left;
 oldright =	right;

 left =	 left/.{K^n_?OddQ->F^(n-1) K};
 right=	right/.{K^n_?OddQ->F^(n-1) K};
 left =	 left/.{K^n_?EvenQ->F^n};
 right=	right/.{K^n_?EvenQ->F^n};

 If[showproof,
 	If[Together[left-oldleft]=!=0 || Together[right-oldright]=!=0,
	   Print["Replacing K^2 by F^2 gives:"];
	   Print[op[left,right]];
	  ];
   ];
  ];

trigRules =
	{
		Sin[A]->2K/(b c),
		Sin[B]->2K/(c a),
		Sin[C]->2K/(a b),
		Cos[A]->(b^2+c^2-a^2)/(2*b*c),
		Cos[B]->(c^2+a^2-b^2)/(2*c*a),
		Cos[C]->(a^2+b^2-c^2)/(2*a*b),
		Tan[A]->4K/(b^2+c^2-a^2),
		Tan[B]->4K/(c^2+a^2-b^2),
		Tan[C]->4K/(a^2+b^2-c^2),
		Csc[A]->(b c)/(2K),
		Csc[B]->(c a)/(2K),
		Csc[C]->(a b)/(2K),
		Sec[A]->(2*b*c)/(b^2+c^2-a^2),
		Sec[B]->(2*c*a)/(c^2+a^2-b^2),
		Sec[C]->(2*a*b)/(a^2+b^2-c^2),
		Cot[A]->(b^2+c^2-a^2)/(4K),
		Cot[B]->(c^2+a^2-b^2)/(4K),
		Cot[C]->(a^2+b^2-c^2)/(4K)
	};

handleTrig[]:=
Block[{oldleft,oldright},

 oldleft =	left;
 oldright =	right;

 left =	 	Expand[left,Trig->True];
 right =	Expand[right,Trig->True];

 If[showproof &&
 	(Together[left-oldleft]=!=0 || Together[right-oldright]=!=0),
     	Print["Expanding the trigonometric expressions gives:"];
		Print[op[left,right]];
   ];

 left = left//.trigRules;
 right = right//.trigRules;

 If[showproof,
 	Print["Removing the trigonometric expressions gives:"];
	Print[op[left,right]];
   ];

 triclearfractions[];
 collect[];
 trigcdize[];
 collect[];

 ];

triclearfractions[]:=
 (* Implicit arguments: left, right, op, showproof. *)
Block[{dl,dr,prod},

 left =	Together[left];
 right =Together[right];
 dl =	Denominator[left];
 dr =	Denominator[right];
 prod =	PolynomialLCM[dl,dr];

 positivize[];

 If[prod=!=1,
   	 left =		Numerator[left]*(prod/dl);
	 right =	Numerator[right]*(prod/dr);
	 left =		Together[left];
	 right =	Together[right];
	 If[showproof,
	 	Print["we can multiply both sides by ",
	 		Factor[prod]," to get:"];
	 	Print[op[left,right]];
	   ];
   ];

 ];

positivize[]:=
 (* implicit inputs: prod, showproof. *)
Block[{saveshowproof,saveshowreason,savebanner},

	If[NumberQ[prod] && prod>0, Return[True]];

    saveshowproof =	showproof;
    saveshowreason =showreason;
    savebanner =	supressbanner;
	If[showAllSteps=!=True,
    	showproof =		False;
    	showreason =	False;
    	supressbanner =	True;
	  ];

 If[trineq[prod>=0]===True,
	If[saveshowproof,Print["Since ",prod," is positive,"]];
 (* else *),
 	If[trineq[prod<=0]===True,
		If[saveshowproof,
			Print["Since ",prod," is negative,"];
			prod = -prod;
		  ];
	(* else *),
	 	Print["Warning: could not determine sign of ",prod,"."];
	  ];
	];

    showproof =		saveshowproof;
    showreason =	saveshowreason;
    supressbanner =	savebanner;

 Return[True];

 ];

trigcdize[]:=
 (* Implicit arguments: left, right, op, showproof. *)
Block[{prod,pr,fulleq,flist,sqFactor,i,fact,expo},

 If[left==0 || right==0,Return[True]];

 prod =	PolynomialGCD[left,right];

 positivize[];

 If[prod=!=1,
    left =	Together[left/prod];
	right =	Together[right/prod];
	If[showproof,
		Print["we can divide both sides by ",Factor[prod]," to get:"];
		Print[op[left,right]];
	  ];
	If[!NumberQ[prod],collect[]];
   ];
 
 (*
  *		See if any squared factors can be removed.
  *)
 
 sqFactor = 1;
 fulleq = left - right;
 flist = FactorSquareFreeList[fulleq];
 For[i=1, i<=Length[flist], i++,
 	{fact,expo} = flist[[i]];
 	If[expo<=1,Continue[]];
 	If[OddQ[expo],expo--];
 	sqFactor = sqFactor * fact^expo;
    ];

 If[sqFactor=!=1,
 	left = Cancel[fulleq/sqFactor];
 	right = 0;
 	If[showproof,
 		Print["Bringing all terms to the left and factoring gives:"];
 		Print[op[Factor[fulleq],0]];
 		Print["Dividing out by the perfect square, ",sqFactor];
 		Print["yields:"];
 		Print[op[left,0]];
 	  ];
 	collect[];
   ];
 
 expr = op[left,right];
 
 If[expr===True || expr===False,
 	Return[expr],
 	Return[notsure]
   ];
 
 ];