proposition: Lemma height_non_negative : forall s `{!Avl s}, height s >= 0.
proof: Proof. induction s; simpl; intros; auto with zarith. inv_avl; intuition; lia_max. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)