proposition: Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s).
proof: Proof. intros; unfold elements; apply elements_aux_sort; auto. intros; inversion H0. Qed.
imports: FunInd FMapInterface FMapList ZArith Int