proposition: Lemma split_avl : forall m x, avl m -> avl (split x m)#l /\ avl (split x m)#r.
proof: Proof. intros m x; functional induction (split x m); simpl; auto. - rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition. - simpl; inversion_clear 1; auto. - rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia