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