Single and double rotations proved to produce balanced trees!
Single and double rotations proved to produce balanced trees!

A few tactics are defined to automatically generate constraints, and rewrite everything to a form omega can solve. With the help these tactics, we can prove that single and double rotations indeed produce balanced trees even if we don't understand how the arithmetics exactly work there (and I don't!).

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