github.com/coq/opam-coq-archive
A set of tactics to deal with inequalities in Coq over N, Z and R:
opam install coq-poltac.0.8.12