proposition: Lemma split_avl : forall s x `{!Avl s}, Avl (t_left (split x s)) /\ Avl (t_right (split x s)).
proof: Proof. intros s x. functional induction (split x s); simpl; auto. - intros. inv_avl; auto. - mysubst; simpl in *; inversion_clear 1; intuition (auto with map typeclass_instances). - mysubst; simpl in *; inversion_clear 1; intuition (auto with map typeclass_instances). Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)