proposition: Theorem cover_min_ex : forall l : list (btree A), l <> [] -> exists t : btree A, cover_min l t.
proof: Proof. intros l H; generalize (find_min_correct (btree A) (weight_tree f) (all_cover _ l)). case (find_min (weight_tree f) (all_cover _ l)). intros p; case p. intros n b ((H1, H2), H3); exists b; auto. split; auto. apply all_cover_cover; auto. intros t2 H4; apply H3. apply cover_all_cover; auto. intros H0. case (one_cover_ex _ l); auto. intros x H1; absurd (In x (all_cover A l)). rewrite H0; simpl in |- *; red in |- *; intros H2; case H2. apply cover_all_cover; auto. Qed.
imports: Coq(Sorting.Permutation)