A way to choose on which variable the induction tactic is applied

[qbuzet]

When we have things like opaque symbol m n p : ..., it may be useful in some case to do things like induction p instead of changing the definition of the lemma in opaque symbol p m n. Another solution may be to have a tactic to swap universal connectors when it is possible.