proposition: Lemma remove_min_avl : forall l x e r h, avl (Node l x e r h) -> avl (remove_min l x e r)#1.
proof: Proof. intros; generalize (remove_min_avl_1 H); intuition. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia