small typeclass generalisations
some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous
more messy proofs redone, and new material
new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
tuned -- avoid spurious exception trace for "the";