proposition: Lemma add_comm : forall e1 e2 s, eq_set (add e1 (add e2 s)) (add e2 (add e1 s)).
proof: Proof. intros e1 e2 s e; split; intro H. destruct (add_12 _ _ _ H) as [e_eq_e1 | e_in_e2_s]. apply add_2; subst; apply add_1. destruct (add_12 _ _ _ e_in_e2_s) as [e_eq_e2 | e_in_s]. subst; apply add_1. do 2 apply add_2; trivial. destruct (add_12 _ _ _ H) as [e_eq_e2 | e_in_e1_s]. apply add_2; subst; apply add_1. destruct (add_12 _ _ _ e_in_e1_s) as [e_eq_e1 | e_in_s]. subst; apply add_1. do 2 apply add_2; trivial. Qed.
imports: List more_list list_permut Arith