proposition: Theorem cover_min_one : forall t : btree A, cover_min (t :: []) t.
proof: Proof. intros t; split; auto. intros t2 H; inversion H; auto. generalize (Permutation_length H0); simpl in |- *; intros; discriminate. Qed.
imports: Coq(Sorting.Permutation)