Ltac finish := auto with between between_no_eauto col le out par perp cong midpoint side conga lea
                          suma sums circle cop.

Create HintDb between.
Create HintDb between_no_eauto.
Create HintDb col.
Create HintDb le.
Create HintDb out.
Create HintDb par.
Create HintDb perp.
Create HintDb cong.
Create HintDb midpoint.
Create HintDb side.
Create HintDb conga.
Create HintDb lea.
Create HintDb suma.
Create HintDb sums.
Create HintDb circle.
Create HintDb cop.