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. intro s1; case s1; clear s1; intros l1 wr1. intro s2; case s2; clear s2; intros l2 wr2. revert l1 wr1 l2 wr2; unfold without_red, cardinal, subset, mem; simpl. fix subset_cardinal_not_eq_not_eq_set 1. intros l1 wr1 l2 wr2 a l1_in_l2 a_not_in_l1 a_in_l2. case (mem_split_set _ _ eq_bool_ok _ _ a_in_l2); intros a' M; case M; clear M. intros l2' M; case M; clear M. intros l2'' M; case M; clear M. intros a_eq_a' M; case M; clear M. intros M _; subst l2. rewrite length_app; simpl (length (a' :: l2'')); rewrite <- plus_n_Sm; rewrite <- length_app. assert (wr2' : without_red (l2' ++ l2'')). apply without_red_remove with a'; assumption. apply le_n_S; apply (@cardinal_subset (mk_set wr1) (mk_set wr2')). intros e; unfold mem; simpl; intro e_in_l1. assert (e_in_l2 := l1_in_l2 e e_in_l1). rewrite <- mem_or_app in e_in_l2; case e_in_l2; clear e_in_l2. intro e_in_l2'; rewrite <- mem_or_app; left; assumption. simpl; intro e_in_l2; case e_in_l2; clear e_in_l2. intro e_eq_a'; absurd (more_list.mem eq_A a l1). assumption. apply (mem_eq_mem eq_proof a'). apply (equiv_sym _ _ eq_proof); assumption. apply (mem_eq_mem eq_proof e); assumption. intro e_in_l2''; rewrite <- mem_or_app; right; assumption. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)