Implement "prover with additional constructions"

[geometer]

With an exhaustive search of possible additional constructions (there should be a set of such constructions) implement a prover that tries to add construction and deduct the goal in the new extended scene. It should be combined with "prover with assumptions" (#7) to make a final product.

In a real planimetry task, there should be enough to add a very limited number of assumptions and/or constructions to deduct the goal.