proposition: Lemma permutation_all_permutations_aux : forall (n : nat) (l1 l2 : list A), n = length l2 -> Permutation l1 l2 -> In l1 (all_permutations_aux l2 n).
proof: Proof. intros n; elim n; simpl in |- *; auto. intros l1 l2; case l2. intros H H0; rewrite (Permutation_nil (Permutation_sym H0)); auto with datatypes. simpl in |- *; intros; discriminate. intros n0 H l1; case l1. intros l2 H0 H1; rewrite (Permutation_nil H1) in H0; discriminate. clear l1; intros a1 l1 l2 H1 H2. case (split_one_in_ex a1 l2); auto. apply Permutation_in with (1 := H2); auto with datatypes. intros x H0. apply in_flat_map with (b := (a1, x)); auto. apply in_map; simpl in |- *. apply H; auto. apply eq_add_S. apply trans_equal with (1 := H1). change (length l2 = length (a1 :: x)) in |- *. apply Permutation_length; auto. apply Permutation_sym; apply split_one_permutation; auto. apply Permutation_cons_inv with (a := a1). apply perm_trans with (1 := H2). apply Permutation_sym; apply split_one_permutation; auto. Qed.
imports: List ListAux