Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique

Patch by Stepan Holub, plus tweaks

patch to vector_matrix_mult by Alexander Pach

try0: cleaned up output;

try0: insert extra facts into state instead of goal, since some methods (e.g. metis) won't work otherwise;

avoid informatik.tu-muenchen.de domain: soon to be discontinued;

renamed Discrete -> Discrete_Functions to avoid name clashes; new function names floor_log/sqrt to avoid long Discrete_Functions.log/sqrt

Use Var to maintain the difference between function and locale parameters

tuned

tuned proofs;