Switched to componentwise relations. Now working on properties of folds.
Ported all relational reasoning combinators to componentwise relations.
Ready to revise the Greedy Theorem.
Proved some properties of preorders and componentwise join.
Should switch to a better behaved join.
Switched (back) to a "regularly shaped" componentwise join.
More properties of join.
Renamed //-preserves-comp to //-preserves-comp' (as it's not exactly preservation of composition).
Mixing plain relations and families of relations proved to be too difficult. For the minimum coin change problem, however, the existing, componentwise version of the greedy theorem suffices. Leaving a more general greedy theorem with componentwise join as future work.