proposition: Lemma without_red_remove_red : forall l, without_red (remove_red l).
proof: Proof. intro l; induction l as [ | e le]; simpl; trivial. destruct (In_dec eq_elt_dec e le) as [ in_e_le | not_in_e_le]; trivial. simpl; destruct (In_dec eq_elt_dec e (remove_red le)) as [ in_e_rrle | _]; trivial; absurd (In e le); trivial; apply included_remove_red; trivial. Qed.
imports: List more_list list_permut Arith