add minimal Proof using annotations modulo Set Default Proof Using

[palmskog]

This commit adds Set Default Proof Using commands in all files with sections, and minimal Proof using annotations to include section hypotheses. This has the following results:

• documents whenever a section hypothesis (in Prop) is used in a proof, as per recent guidelines
• makes it worthwhile to use make vio or make vos on the project (build time is nearly halved)

Finally, I added one missing Proof and removed a redundant Proof, discoveries that were made on the way.

[chdoc]

I think that if everything in a section depends on a section hypothesis, then it it preferable to state this once (via Local Set Proof Using) rather than have this said again and again, possibly leading to over-length one-line proofs. For mult-line proofs this is less of an issue, because there is plenty of space after the Proof. I pushed what I had in mind, are you okay with that? (I also removed count_nseq which is indeed in mathcomp since at least 1.9.0, albeit with a slightly more general type.)

[palmskog]

Your changes look fine to me, feel free to merge.