Insert indeed adds the element to the tree.
Insert indeed adds the element to the tree.

I skipped the proof for balanceR part because the [inset_balanceR] lemma we need is just going to be like [inset_balanceL], and the proof for the latter one is way too tedious... I'm seeking for ways to automate more in that proof before diving into [inset_balanceR].

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