sugestion/discussion for a `contra:` tactic

Being a frequent user of contra_ lemmas I wonder whether there would be a way to avoid having a separate lemma for every combination of (decidable) predicates (cf. #578), and instead have a tactic contra: such that contra: H looks at the goal and applies canonical/registered negations to both premise and conclusion of the resulting implication.

Unfortunately, some predicates can be negated in several ways, e.g. n <= m can be negated as m < n, ~~ (n <= m) or even ~(n <= m) by applying different contra lemmas. So this alone may not solve the problem completely.

my suggestion is to make contra a generic lemma using canonical structures / typeclass attaching a negation to each construct. So that one can use apply: contra H in any case.