proposition: Lemma concat_avl : forall m1 m2, avl m1 -> avl m2 -> avl (concat m1 m2).
proof: Proof. intros m1 m2; functional induction (concat m1 m2); auto. intros; apply join_avl; auto. generalize (remove_min_avl H0); rewrite e1; simpl; auto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia