Disambiguate precedence in negbLR and negbRL and add new lemmas for left and right distributivity

[oskgo]

Fixes #732

[oskgo]

I'm not surprised that there's third party breakage here. This is a breaking change to a prelude theory.

How do I proceed? @strub?

[fdupress]

Ping the maintainer, which we really should add to the config.

Fortunately, I'm the maintainer here. Will fix when I have some time.

[fdupress]

So the fix, as expected, is not a valid proof in current main. We have two options:

1. Stage the fix across two releases: first add the new lemma names, allowing smooth proof fixes; then change the lemma statements for the old lemma names;
2. Ship it and issue a clear warning that this is coming, and how to fix it, to the Formosa meeting and via our other communication channels (including release notes).

As you know, Matthias and I put some work into figuring out how to enable 2 safely, so I'm completely fine with 2. But we have users whose proofs are not in the external CI.

Pierre-Yves @strub, thoughts? (And those thoughts should become policy at some point.)
Note also that the situation here is slightly different from #727:

• this PR can be staged, Reworked outline tactic #727 can't easily be staged;
• this PR breaks a long-standing behaviour, Reworked outline tactic #727 should only affect very early adopters (proofs started in the last ~9 months).

This policy discussion should probably be moved off this issue.