proposition: Lemma subset_cardinal : forall s s', s[<=]s' -> cardinal s <= cardinal s' .
proof: Proof. intros. rewrite <- (diff_inter_cardinal s' s). rewrite (inter_sym s' s). rewrite (inter_subset_equal H). apply Nat.le_add_l. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide