proposition: Lemma in_permut_in : forall l1 l2 e, In e l1 -> list_permut l1 l2 -> In e l2.
proof: Proof. unfold list_permut, meq; intros l1 l2 e Inel1 Pl1l2. elim (In_dec eq_elt_dec e l2). intros; trivial. intro notInel2; generalize (Pl1l2 e); rewrite (out_mult_O e l2 notInel2); intro M0; generalize (in_mult_S e l1 Inel1); rewrite M0; unfold ge; intro Abs; absurd (1<=0); trivial; inversion Abs. Qed.
imports: decidable_set List more_list Multiset Arith Setoid