proposition: Lemma all_permutations_aux_permutation : forall (n : nat) (l1 l2 : list A), n = length l2 -> In l1 (all_permutations_aux l2 n) -> Permutation l1 l2.
proof: Proof. intros n; elim n; simpl in |- *; auto. intros l1 l2; case l2. simpl in |- *; intros H0 [H1| H1]. rewrite <- H1; auto. case H1. simpl in |- *; intros; discriminate. intros n0 H l1 l2 H0 H1. case in_flat_map_ex with (1 := H1). clear H1; intros x; case x; clear x; intros a1 l3 (H1, H2). case in_map_inv with (1 := H2). simpl in |- *; intros y (H3, H4). rewrite H4; auto. apply perm_trans with (a1 :: l3); auto. apply perm_skip; auto. apply H with (2 := H3). apply eq_add_S. apply trans_equal with (1 := H0). change (length l2 = length (a1 :: l3)) in |- *. apply Permutation_length; auto. apply Permutation_sym; apply split_one_permutation; auto. apply split_one_permutation; auto. Qed.
imports: List ListAux