proposition: Lemma flatten_e_elements : forall l x r c e, elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e.
proof: Proof. intros. now rewrite elements_node, <- app_assoc. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat