proposition: Lemma list_permut_dec : forall l1 l2, {list_permut l1 l2}+{~list_permut l1 l2}.
proof: Proof. intro l1; induction l1 as [ | e1 l1]. destruct l2 as [ | e2 l2]. left; apply list_permut_refl. right; intro P; assert (H := list_permut_length P); discriminate. intro l2; destruct (In_dec eq_elt_dec e1 l2) as [e1_in_l2 | e1_not_in_l2]. generalize (split_list_app_cons eq_elt_dec _ _ e1_in_l2); clear e1_in_l2; destruct (split_list eq_elt_dec l2 e1) as [l2' l2'']; intro; subst. destruct (IHl1 (l2' ++ l2'')) as [P | nP]. left; apply list_permut_add_cons_inside; trivial. right; intro P; apply nP; apply list_permut_remove_hd with e1; trivial. right; intro P; apply e1_not_in_l2; apply in_permut_in with (e1 :: l1); trivial; left; trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid