Some work on balanceL.
Some work on balanceL.

Arithmetic part is a pain. But really the arithmetic here is equivalent to nat arithmetic (no negative number, no minus operation). Is there a good way to reflect the arithmetic to Nat?

antalsz/hs-to-coq,antalsz/hs-to-coq