proposition: Lemma without_red_add : forall e l1 l2, without_red (l1 ++ l2) -> ~In e (l1 ++ l2) -> without_red (l1 ++ e :: l2).
proof: Proof. intros e l1; generalize e; clear e; induction l1 as [ | e1 l1]; intros e l2 wr12 e_not_in_l1_l2. simpl; destruct (In_dec eq_elt_dec e l2) as [e_in_l2 | _]; trivial. absurd (In e l2); trivial. simpl. destruct (In_dec eq_elt_dec e1 (l1 ++ e :: l2)) as [e1_in_l1_e_l2 | e_not_in_l1_e_l2]. destruct (in_app_or _ _ _ e1_in_l1_e_l2) as [e1_in_l1 | [e1_eq_e | e1_in_l2]]. simpl in wr12; destruct (In_dec eq_elt_dec e1 (l1 ++ l2)) as [e1_in_l1_l2 | e1_not_in_l1_l2]. trivial. absurd (In e1 (l1 ++ l2)); trivial; apply in_or_app; left; trivial. subst e; absurd (In e1 ((e1 :: l1) ++ l2)); trivial; left; trivial. simpl in wr12; destruct (In_dec eq_elt_dec e1 (l1 ++ l2)) as [e1_in_l1_l2 | e1_not_in_l1_l2]. trivial. absurd (In e1 (l1 ++ l2)); trivial; apply in_or_app; right; trivial. apply IHl1. apply (without_red_remove e1 nil (l1 ++ l2)); trivial. intro e_in_l1_l2; apply e_not_in_l1_l2; right; trivial. Qed.
imports: List more_list list_permut Arith