… attribute

From explanations and experiments by Simon, Gabriel and Kenny at
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cc.20is.20so.20powerful

A short guide on getting started with Lean, mathlib and elan.
Adds a link to docs/elan.md in README.md

…nity#105)

…im (leanprover-community#108)

…y#116)

... but which generates equality proof obligations for every discrepancy between the goal and
the type of the rule

…ructures

…ies to assumptions (leanprover-community#110)

…sets is compact (leanprover-community#117)

for removing identity junk and annotations added to terms by common tactics like dsimp

…el's leanprover-community#115)

…ear_order -> conditionally_complete_linear_order; add cSup/cInf_interval

…extive/transitive relations & use them for the free group reduction

…ions of limit type

leanprover-community#131)

…ives using logical connectives

…guments; show that eval is ring homomorphism

(closes leanprover-community#134)

…nish was very slow)

Patch 10