proposition: Lemma without_red_remove : forall e l1 l2, without_red (l1 ++ e :: l2) -> without_red (l1 ++ l2).
proof: Proof. intros e l1; generalize e; clear e; induction l1 as [ | e1 l1]; intros e l2; simpl. destruct (In_dec eq_elt_dec e l2); trivial; contradiction. destruct (In_dec eq_elt_dec e1 (l1 ++ e :: l2)) as [ | not_in_e1]. contradiction. destruct (In_dec eq_elt_dec e1 (l1 ++ l2)) as [ in_e1 | _]. intros _; apply not_in_e1; generalize (@in_app_or _ _ _ _ in_e1); clear in_e1; intros [ in_e1 | in_e1]; apply in_or_app; [left | right; right]; trivial. intro; apply (IHl1 e l2); trivial. Qed.
imports: List more_list list_permut Arith