[ refactor ] reorganise Relation.Nullary.Negation.Core to make clean separation of properties

[jamesmckinna]

This is somehow an 'intermediate' PR following on from #2803 and before the more radical #2802 , aiming to systematise the organisation of the module into definitions and properties which depend on negation being a connective in minimal logic, and those (fewer, but more powerful) which genuinely rely on ex falso in the form of Data.Empty.⊥-elim.

NB. More in the same spirit may be possible downstream, eg.

• monadic structure on DoubleNegation requires only the minimal properties (modulo definitional proof-irrelevance... which now could also be tackled by [ refactor ] make contradiction and friends entirely definitionally proof-irrelevant #2802 )
• more nuanced consideration of the style-guide recommendations in [ add ] style-guide recommendation preferring contradiction over ⊥-elim #2798
• etc.

[JacquesCarette]

I like the reorganization and additional comments. I would approve that.

I'm only requesting changes because you've touched something that now seems pointless, so you've taken on the burden of needing to justify why it's still there!