proposition: Theorem build_cover : forall l t, build l t -> cover l t.
proof: Proof. intros l t H; elim H; clear H l t; auto. intros t l1 l2 (l3, (t1, (t2, (HH, (HH1, HH2))))) H0 H1; try assumption. apply cover_node with (1 := HH1); auto. apply cover_permutation with (2 := HH2); auto. Qed.
imports: Coq(ArithRing Sorting.Permutation)