proposition: Lemma subset_cardinal_lt : forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s'.
proof: Proof. intros. rewrite <- (diff_inter_cardinal s' s). rewrite (inter_sym s' s). rewrite (inter_subset_equal H). generalize (@cardinal_inv_1 (diff s' s)). destruct (cardinal (diff s' s)). - intro H2; destruct (H2 Logic.eq_refl x). set_iff; auto. - intros _. change (0 + cardinal s < S n + cardinal s). apply Nat.add_lt_le_mono; [ apply Nat.lt_0_succ | reflexivity ]. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide