A negation is no longer answered with the empty set (#1127)

[Rafael-SOWNet]

Closes #1127.

The defect

StatementSolver.Solve has arms for equality, the connectives, the four comparisons, membership,
provided and piecewise. It had none for not, so every negation fell through to
_ => Set.Empty.

The empty set is a positive claim — no x satisfies this — and it was false of all of these:

"not (x = 1)".ToEntity().Solve("x")             {  }
"not (x > 1)".ToEntity().Solve("x")             {  }
"not (x >= 1)".ToEntity().Solve("x")            {  }
"not not (x = 1)".ToEntity().Solve("x")         {  }
"not (x > 1 or x < -1)".ToEntity().Solve("x")   {  }
"not (x in RR)".ToEntity().Solve("x")           {  }

This is the defect #1036 fixed for equations, left standing for negation.

The fix

The negation is pushed inward as far as there is an arm for it, and named as a set-builder where
there is not:

"not (x = 1)".ToEntity().Solve("x")             { x : not x = 1 }
"not (x > 1)".ToEntity().Solve("x")             (-oo; 1]
"not (x >= 1)".ToEntity().Solve("x")            (-oo; 1)
"not not (x = 1)".ToEntity().Solve("x")         { 1 }
"not (x > 1 or x < -1)".ToEntity().Solve("x")   [-1; 1]
"not (x in RR)".ToEntity().Solve("x")           { x : not x in RR }

Three things, in order:

1. Double negation and De Morgan, pushing the negation towards the leaves. Inward is
   unambiguous here in a way it is not in the simplifier — where it can grow an expression, which
   is why no rule set does it — and that is the reason it lives in the solver: this switch has arms
   for the connectives and for the comparisons and none for not, so inward is the direction that
   reaches one.
2. A negated comparison is a comparison, and RewriteRules.InequalityEquality is where that is
   already written down. Asking it rather than restating it keeps the two from drifting.
3. What neither reaches is answered as written — the shape Domain.Any is a codomain and not the universal set (#996) #1126 introduced for implications.
   { x : not x in RR } names the non-real complex numbers exactly and asserts of them only what
   the statement says.

Tests

26, in NegationIsNotTheEmptySetTest. They assert which values the answers admit rather than
the shape the answers are written in, so a later rewrite that says the same thing better does not
fail them — not (x > 1) is checked to contain 0 and 1 and not 5, and to equal the answer to
x <= 1, rather than to print as (-oo; 1].

21 of the 26 fail against the previous behaviour.

Measured

• Unit suite 9211 passed, 1 failed — OneSidedLimitTest.ADifferenceOfReciprocalLogarithms(side: Left),
  which fails identically on plain master with none of this branch's changes, and passes when
  run alone. Controlled for by running the full suite on master at 5351d0cf: same one failure,
  9185 passed. Pre-existing, and not something this branch touches.
• Two BREAKING-CHANGES.md entries, both measured on a build.