proposition: Lemma height_0 : forall s `{!Avl s}, height s = 0 -> s = Leaf _.
proof: Proof. destruct 1; avl2Avl; intuition; simpl in *. avl_nns. simpl in *; exfalso; lia_max. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)