proposition: Lemma without_red_filter_aux : forall P P_dec l, without_red l -> without_red (filter_aux P P_dec l).
proof: Proof. intros P P_dec l; induction l as [ | e le]; simpl; trivial. destruct (P_dec e) as [ _ | _ ]; destruct (In_dec eq_elt_dec e le) as [ in_e_le | not_in_e_le]; trivial; try contradiction. simpl; destruct (In_dec eq_elt_dec e (filter_aux P P_dec le)) as [ in_e_rrle | _]; trivial; absurd (In e le); trivial. apply included_filter_aux with P P_dec; trivial. Qed.
imports: List more_list list_permut Arith