small inversions in the standard library

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4989
From: @JasonGross
Reported version: trunk
CC: @andersk

See also: BZ#4891

[coqbot]

Comment author: @JasonGross

I'd like to see a tactic for small inversions
(http://gallium.inria.fr/blog/a-new-Coq-tactic-for-inversion/,
http://www-verimag.imag.fr/~monin/Proof/SmallInvScalesUp/paper.pdf) make its
way into the standard library.

[maximedenes]

@herbelin mentioned during the WG he's working on it (with Thierry Martinez), so assigning to him.

[Zimmi48]

In the last Coq Call, @maximedenes or @ybertot (I don't remember) asked for some specific users wanting this feature. It seems from #17099 that @mukeshtiwari is one.