feat(emacs/lean-flycheck): detect and use flycheck error buffer width

Detect the width of flycheck error list buffer and set pp.width when
calling flycheck. It uses the same heuristic that `split-window-sensibly`
function is using.

A user can also set `lean-flycheck-msg-width` custom variable to enforce
a certain width.

Close #205.
refactor(library): mark 'decidable' theorems as definitions

If we don't do that, then any 'if' term that uses one of these theorems
will get "stuck". That is, the kernel will not be able to reduce them
because theorems are always opaque