CindyJS

Pappos's Theorem

We will use create(["II"], "Meet", ["g", "h"]); to generate a point which is already present ("I"). The prover will drop it.