Implement "prover with assumptions"

[geometer]

If the direct prover fails (i.e., stops with no proof for the goal), it should

• select a fact that could have different answers, e.g. "the point lies on the circle", "the point lies inside the circle", and "the point lies outside of the circle";
• consequentially run direct provers starting with the property set + one of the assumptions;
• each run generates one of the following results: (1) the goal is proven, (2) a contradiction found, (3) no result, and (4) failure: the prover generates an assertion error;
• if all the results are of type (1) or (2), and at least one of them is of type (1), we have proof;
• otherwise, select or add another fact.

See also #10 for the next step.