Got one step further with step_inc
Now the 2 proofs about step both get stuck at the same point.

Started proving foldl1_is_min by introducing a lot of sub-lemmas.
Except for join_pairs they should all be trivial.
join_pairs we should work out using lemma1 or some alternative.