proposition: Lemma filter_1_list : forall (P : elt -> Prop) P_dec l e, In e l -> P e -> In e (filter_aux P P_dec l).
proof: Proof. intros P P_dec l; induction l as [ | e' l ]. contradiction. intros e [e_eq_e' | e_in_l] Pe. subst e'; simpl. destruct (P_dec e) as [ _ | not_Pe]. left; trivial. absurd (P e); trivial. simpl; destruct (P_dec e') as [ _ | _ ]; [ right | idtac ]; apply IHl; trivial. Qed.
imports: List more_list list_permut Arith