The math package

[Sventimir]

Following discussion under #1727 I have extracted math-related stuff from contrib into its own package called math. My criteria for including a module in math were twofold:

1. It's related to a numeric type defined in the standard library (i.e not built into the language) or defines such types.
2. It contains (ideally exclusively) definitions or proofs of properties of these types.

This is meant to be mostly a library of proofs, so it makes little sense to include modules related to built-in types like Integer. It's purposes are threefold:

1. Demonstrate the ability of Idris as a proof-assistant;
2. Provide a place for people interested in theorem proving in Idris to put their proofs in;
3. In the long term, provide an extensive library of proofs of properties of basic numeric types that can be used to describe and prove properties of practical programs more easily.

I'm not entirely sure if I tracked down all the modules in contrib that fulfill my criteria. If there are some that I missed, I'm happy to include them as well.

[nickdrozd]

Seems like a reasonable compromise between leaving the math stuff strewn about contrib and cutting it entirely.

[andrevidela]

It looks like this has diverged a little bit. I suspect it's because none of us are really willing to touch the libraries until we've found a real consensus. @Sventimir would you be ok postponing this PR until the developper meetup in december? I encourage you to talk about it with everyone else there

[Sventimir]

Yep, I', fine with that. However, I have no idea if I'll be able to attend the meeting at this point. I'm having other occupations than Idris recently. Closing the PR.