proposition: Lemma included_filter_aux : forall P P_dec e l, In e (filter_aux P P_dec l) -> In e l.
proof: Proof. intros P P_dec x l; induction l as [ | e le ]. contradiction. simpl; destruct (P_dec e) as [ _ | _]. intros [x_eq_e | x_in_rrle]; simpl. left; trivial. right; apply IHle; trivial. intro; right; apply IHle; trivial. Qed.
imports: List more_list list_permut Arith