proposition: Theorem ordered_cover_height_pred : forall (n : nat) (t : btree A) (l : list (btree A)), ordered_cover l t -> exists ln : list nat, height_pred n ln l t.
proof: Proof. intros n t l H; generalize n; elim H; clear n t l H. intros t l n; exists (n :: []); auto. intros t1 t2 l1 l2 l3 H H0 H1 H2 n. case (H0 (S n)); intros ln1 HH1. case (H2 (S n)); intros ln2 HH2. exists (ln1 ++ ln2); auto. Qed.
imports: Coq(ArithRing)