proposition: Lemma subset_cardinal_not_eq_not_eq_set : forall s1 s2 e, subset s1 s2 -> ~mem e s1 -> mem e s2 -> cardinal s1 < cardinal s2.
proof: Proof. intros s1 [l2 wr2]; generalize s1; clear s1. assert (forall l2', l2' = l2 -> length l2' = length l2). intros; subst; trivial. generalize (length l2) H; clear H; intros n H; generalize (H _ (refl_equal _)) wr2; generalize l2; clear l2 wr2 H; induction n; destruct l2 as [ | e2 l2]. contradiction. intro; discriminate. intro; discriminate. intros L wr2 s1 e s1_in_e2_l2 e_not_in_s1 [e_eq_e2 | e_in_l2]. assert (wr2' := without_red_remove e2 nil l2 wr2); simpl in wr2'. injection L; clear L; intro L; generalize (IHn _ L wr2'); clear IHn; intro IHn; subst e. assert (subset s1 (mk_set l2 wr2')). intros e e_in_s1; destruct (s1_in_e2_l2 e e_in_s1) as [e_eq_e2 | e_in_l2]; trivial. absurd (mem e2 s1); subst; trivial. apply le_lt_trans with (cardinal (mk_set l2 wr2')). apply cardinal_subset; trivial. unfold cardinal; simpl; apply lt_n_Sn. generalize (split_list_app_cons eq_elt_dec _ _ e_in_l2). destruct (split_list eq_elt_dec l2 e) as [l2' l2'']; clear e_in_l2. intro; subst l2; assert (wr2' := without_red_remove e (e2 :: l2') l2'' wr2). assert (L' : length (e2 :: l2' ++ l2'') = n). simpl in L; injection L; clear L; rewrite list_app_length; rewrite plus_comm; simpl; rewrite plus_comm; rewrite <- list_app_length; trivial. generalize (IHn _ L' wr2'); clear IHn; intro IHn. assert (subset s1 (mk_set _ wr2')). intros e' e'_in_s1; destruct (s1_in_e2_l2 e' e'_in_s1) as [e'_eq_e2 | e'_in_l2]. subst; left; trivial. destruct (in_app_or _ _ _ e'_in_l2) as [e'_in_l2' | e'_in_e_l2'']. simpl; right; apply in_or_app; left; trivial. destruct e'_in_e_l2'' as [e'_eq_e | e'_in_l2'']. subst e'; absurd (mem e s1); trivial. simpl; right; apply in_or_app; right; trivial. apply le_lt_trans with (cardinal (mk_set _ wr2')). apply cardinal_subset; trivial. unfold cardinal; simpl; apply lt_n_S. do 2 rewrite list_app_length; apply plus_lt_compat_l; simpl; apply lt_n_Sn. Qed.
imports: List more_list list_permut Arith