proposition: Theorem all_cover_aux_cover : forall (n : nat) l t, n = length l -> In t (all_cover_aux l n) -> cover l t.
proof: Proof. intros n; elim n; simpl in |- *; auto. intros l t H H0; elim H0. intros n0 H l t H0 H1. case in_flat_map_ex with (1 := H1); clear H1. intros x; case x; clear x. simpl in |- *; intros (H1, H2); case H2. intros b x; case x; clear x. simpl in |- *; intros (H1, [H2| H2]). rewrite <- H2. rewrite Permutation_length_1_inv with (a := b) (l := l); auto. apply all_permutations_permutation; auto. case H2. intros b1 l1 (H1, H2). apply cover_node with (l2 := l1) (t1 := b) (t2 := b1); auto. apply Permutation_sym; apply all_permutations_permutation; auto. apply H; auto. apply eq_add_S; apply trans_equal with (1 := H0). apply trans_equal with (length (b :: b1 :: l1)); auto. apply Permutation_length. apply Permutation_sym; apply all_permutations_permutation; auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)