refactor(library/logic): add basic definitions for relations at logic/relation.lean

We need them for wf and definitional package
refactor(library/data/nat/sub): cleanup 'max' theorems
test(tests/lean/run/tree_height): experiment with wf relation based on the height

This is easier to generate than the subterm relation
test(tests/lean/run/div_wf): cleanup
test(tests/lean/run/gcd): gcd compiled by hand into wf recursion