proposition: Lemma without_red_add_without_red : forall l1 l2, without_red l1 -> without_red (add_without_red l1 l2).
proof: Proof. intros l1 l2; generalize l1; clear l1; induction l2 as [ | e le]; intros l1 wr1; simpl; trivial. destruct (In_dec eq_elt_dec e l1) as [ _ | not_in_e_l1]; apply IHle; trivial. simpl; destruct (In_dec eq_elt_dec e l1) as [ in_e_l1 | _]; trivial; absurd (In e l1); trivial. Defined.
imports: List more_list list_permut Arith