proposition: Lemma height_non_negative : forall (s : t elt), avl s -> height s >= 0.
proof: Proof. induction s; simpl; intros. - now apply Z.le_ge. - inv avl; intuition; omega_max. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia