proposition: Lemma cardinal_subset : forall s1 s2, subset s1 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 subset, cardinal, mem, without_red; simpl. fix cardinal_subset 1. intro l1; case l1; clear l1. intros _ l2 _ _; apply Nat.le_0_l. simpl; intros a1 l1. generalize (mem_bool_ok _ _ eq_bool_ok a1 l1); case (mem_bool eq_bool a1 l1). intros _ Abs; discriminate. intros a1_not_in_l1 wr1 l2 wr2 l1_in_l2. assert (e1_in_l2 : more_list.mem eq_A a1 l2). apply l1_in_l2; left; reflexivity. case (mem_split_set _ _ eq_bool_ok _ _ e1_in_l2). intros a1' M; case M; clear M. intros l2' M; case M; clear M. intros l2'' M; case M; clear M. intros a1_eq_a1' M; case M; clear M. intros H' _; subst l2. rewrite length_add; simpl; apply le_n_S; apply cardinal_subset. assumption. apply (without_red_remove a1' l2' l2''); assumption. intros e e_in_l1; apply diff_mem_remove with a1'. intro e_eq_a1'; apply a1_not_in_l1. apply (mem_eq_mem eq_proof a1'). apply (equiv_sym _ _ eq_proof); assumption. apply (mem_eq_mem eq_proof e); assumption. apply l1_in_l2; right; assumption. Defined.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)