proposition: Lemma elements_node c l x r : elements (Node c l x r) = elements l ++ x :: elements r.
proof: Proof. unfold elements; simpl. now rewrite !elements_app, !app_nil_r. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat