proposition: Lemma add_Add : forall x s, !!(add x s) === Add _ (!!s) x.
proof: Proof. unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; auto with sets. - inversion H0. constructor 2; constructor. - constructor 1; auto. Qed.
imports: Ensembles Finite_sets MSetInterface MSetProperties OrdersEx