proposition: Theorem one_cover_ex : forall l : list (btree A), l <> [] -> exists t : btree A, cover l t.
proof: Proof. intros l; elim l; simpl in |- *; auto. intros H; case H; auto. intros a l0; case l0; auto. intros H H0; exists a; auto. intros b l1 H H0; case H. red in |- *; intros; discriminate. intros x H1; exists (node a x). apply cover_cons_l; auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)