finer-grained analysis of NonZero arguments

[jamesmckinna]

[Breaking changes so held back from merge of #2182 into v2.1]

Essentially a placeholder DRAFT PR in which to accumulate all such things, towards an eventual v3.0 merge.

NB: currently, the statements/proofs follow a rather clunky

• let instance _ =... in the statements;
• where instance _ = ... in the proofs.

Suggest subsequent refactorings to make all such things anonymous modules which set up all the appropriate scope... esp. in the cases where there are auxiliary lemmas.

UPDATED: @MatthewDaggitt 's review comment gives me pause... So I'll refrain from committing further for the time being!

[jamesmckinna]

Given the negative tone of the comments, and finding myself getting combative/defensive in response to them, maybe the best thing is to close this as status:abandoned (UPDATED: that label seems to have gone!). Also for the second night in a row, I have had less than 3hrs' sleep, so my resources are severely stretched for thinking about this, much less trying to convince the two of you. Oh well.

[JacquesCarette]

"Convincing" me of finicky stuff with instance arguments is perhaps too high a bar. I really don't like instance arguments (but reluctantly admit that for NonZero they are generally a win). Since it has been agreed that NonZero is ok in the library, the only 'argument' left is on the level of acceptable gymnastics that is reasonable locally. And not forcing a proof to have a particular shape.