proposition: Theorem cover_ordered_cover : forall (l1 : list (btree A)) (t : btree A), cover l1 t -> exists l2, Permutation l1 l2 /\ ordered_cover l2 t.
proof: Proof. intros l1; elim l1 using list_length_ind. intros l0 H t; case t. intros a H1; rewrite cover_inv_leaf with (1 := H1). exists (leaf a :: []); auto. intros t1 t2 H1; case cover_inv_app with (1 := H1). intros H2; exists l0; split; auto; rewrite H2; auto. intros (l2, (l3, ((HH1, HH2), HH3))). case H with (2 := HH1); auto. rewrite Permutation_length with (1 := HH3). generalize HH2; rewrite app_length; case l3; simpl in |- *; auto with arith. intros HH4; case cover_not_nil with (1 := HH4); auto. intros; rewrite Nat.add_comm; simpl in |- *; auto with arith. intros l4 (HP1, HP2). case H with (2 := HH2); auto. rewrite Permutation_length with (1 := HH3). generalize HH1; rewrite app_length; case l2; simpl in |- *; auto with arith. intros HH4; case cover_not_nil with (1 := HH4); auto. intros l5 (HP3, HP4). exists (l4 ++ l5); split; auto. apply Permutation_trans with (1 := HH3); auto. Qed.
imports: Coq(Sorting.Permutation)