proposition: Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
proof: Proof. intros; apply bool_1; split; intros. - rewrite MP.cardinal_1; simpl; auto with set. - assert (cardinal s = 0) by (apply zerob_true_elim; auto). auto with set. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx