proposition: Lemma cardinal_union_inter_12 : forall s1 s2, cardinal (union s1 s2) + cardinal (inter s1 s2) = cardinal s1 + cardinal s2.
proof: Proof. assert (H : forall acc l1 l2, length (remove_not_common acc l1 l2) = length acc + length (remove_not_common nil l1 l2)). intros acc l1 l2; generalize acc l1; clear acc l1; induction l2 as [ | e2 l2]; intros acc l1; trivial. simpl; destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1 ]. rewrite (IHl2 (e2 :: acc) l1); rewrite (IHl2 (e2 :: nil) l1); simpl; apply sym_eq; rewrite plus_comm; simpl; rewrite plus_comm; trivial. apply IHl2. assert (H' : forall acc l1 l2 e, ~In e l1 -> ~ In e l2 -> remove_not_common acc (e :: l1) l2 = remove_not_common acc l1 l2). intros acc l1 l2; generalize acc l1; clear acc l1; induction l2 as [ | e2 l2]. simpl; intros acc l1 e e_not_in_l1 _; destruct (In_dec eq_elt_dec e l1) as [ e_in_l1 | _ ]; trivial. intros acc l1 e e_not_in_l1 e_not_in_e2l2; simpl; destruct (eq_elt_dec e e2) as [e_eq_e2 | e_diff_e2]; destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1 ]. apply IHl2; trivial; intro; apply e_not_in_e2l2; right; trivial. subst e; absurd (In e2 (e2 :: l2)); trivial; left; trivial. apply IHl2; trivial; intro; apply e_not_in_e2l2; right; trivial. apply IHl2; trivial; intro; apply e_not_in_e2l2; right; trivial. intros [l1 wr1] [l2 wr2]; unfold cardinal; simpl; generalize l1 wr1; clear l1 wr1; induction l2 as [ | e2 l2]; intros l1 wr1; trivial; simpl; destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1 ]. rewrite H; simpl; rewrite plus_comm; simpl; rewrite plus_comm; rewrite IHl2; trivial. apply (without_red_remove e2 nil l2); trivial. assert (wr1' : without_red (e2 :: l1)). simpl; destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | _ ]; trivial. absurd (In e2 l1); trivial. assert (wr2' := without_red_remove e2 nil l2 wr2); simpl in wr2'. assert (H'' := IHl2 wr2' _ wr1'). rewrite H' in H''; trivial. rewrite H''; apply sym_eq; rewrite plus_comm; simpl; rewrite plus_comm; trivial. simpl in wr2; destruct (In_dec eq_elt_dec e2 l2); trivial; contradiction. Qed.
imports: List more_list list_permut Arith