proposition: Theorem height_pred_ordered_cover : forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)), height_pred n ln l t -> ordered_cover l t.
proof: Proof. intros n ln t l H; elim H; simpl in |- *; auto. Qed.
imports: Coq(ArithRing)