Simplify precondition and unify `balanceL_Desc` and `balanceL_Desc_for_link`
Simplify precondition and unify `balanceL_Desc` and `balanceL_Desc_for_link`

The precondition is dervied by mechanically eliminating the quantifiers
in this system of linear equations. Hooray for having learned about
simplex algorithm (or whatever that was).

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