use lia instead of omega

See merge request robbertkrebbers/coq-stdpp!37

add lemma about chained difference

See merge request robbertkrebbers/coq-stdpp!36

solve_ndisj: try harder

See merge request robbertkrebbers/coq-stdpp!35

Works around Coq bug #7731

add telescopic versions of the Coq quantifiers

See merge request robbertkrebbers/coq-stdpp!34

add telescopes and a bit of theory about them

See merge request robbertkrebbers/coq-stdpp!33

introduce [default] as abbreviation for [from_option id], and use it

See merge request robbertkrebbers/coq-stdpp!32

Remove the `default` notation for options

See merge request robbertkrebbers/coq-stdpp!31

The notation was parsing-only and all it did was reorder the arguments for
from_option.  This creates just a needless divergence between what is written
and what is printed.  Also, removing it frees the name for maybe introducing a
function or notation `default` with a type like `T -> option T -> T`.