proposition: Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
proof: Proof. unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto. apply (is_bst m). Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia