Unify Coq and F* devs

We want to unify the notation and the documentation between Coq and F* developments

TODO

• Renaming in the F* dev #7 (closed)
  • rename Cut to Empty
  • rename is_tall to has_height
  • rename incremental to leftist [x] Pack incremental as single definition in F*, and simplify devs
• Remove the position argument from insert_naive. Rename [insert_naive] to [insert_model]
• Incorporate coqdoc style documentation from the Coq devs

Depends on !7 (merged)