Negating disproved conjectures

Some of the initial formalisations were written following the convention of sticking to the original formulation, even though it is known to be false, i.e. in this convention the statement "Prove proposition `P`" is always formalised as
```
theorem foo : P := sorry
```
even when `P` has been (informally) disproven (in which case "solving the problem" means diproving the formal statement rather than proving it).

We have moved to the convention of replacing `P` by its negation when it is known to be false, so a small number of formalisations will need to be changed to follow that style.