proposition: Lemma subset_set_diff : forall s1 s2 s2', subset s2 s2' -> cardinal (set_diff s1 s2') <= cardinal (set_diff s1 s2).
proof: Proof. unfold set_diff, filter, cardinal; simpl. intros [s1 prf]; simpl; induction s1 as [ | a1 s1]; intros s2 s2' s2_in_s2'; simpl. apply le_n. assert (prf1 := without_red_remove a1 nil s1 prf); simpl in prf1. assert (H := IHs1 prf1 _ _ s2_in_s2'). set (l := filter_aux (fun e : EDS1.A => negb (mem_bool EDS1.eq_bool e (support s2))) s1) in *. set (l' := filter_aux (fun e : EDS1.A => negb (mem_bool EDS1.eq_bool e (support s2'))) s1) in *. generalize (s2_in_s2' a1); unfold mem. generalize (mem_bool_ok _ _ eq_bool_ok a1 (support s2)). generalize (mem_bool_ok _ _ eq_bool_ok a1 (support s2')). case (mem_bool EDS1.eq_bool a1 (support s2')). case (mem_bool EDS1.eq_bool a1 (support s2)). intros _ _ _; assumption. intros _ _ _; simpl; apply le_S; assumption. case (mem_bool EDS1.eq_bool a1 (support s2)); simpl. intros a1_not_in_s2' a1_in_s2 Sub; apply False_rect. apply a1_not_in_s2'; apply Sub; apply a1_in_s2. intros _ _ _; apply le_n_S; assumption. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)