proposition: Theorem height_pred_larger_ex : forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)), height_pred n ln l t -> exists n1, In n1 ln /\ n <= n1.
proof: Proof. intros n ln t l H; elim H; clear H n ln t l. intros n t; exists n; auto with datatypes. intros n ln1 ln2 t1 t2 l1 l2 H (n1, (HH1, HH2)) H1 H2. exists n1; auto with datatypes arith. Qed.
imports: Coq(ArithRing)