proposition: Theorem height_pred_larger : forall (n n1 : nat) (ln : list nat) (t : btree A) (l : list (btree A)), height_pred n ln l t -> In n1 ln -> n <= n1.
proof: Proof. intros n n1 ln t l H; generalize n1; elim H; clear H n ln t l n1; auto with arith. intros n t n1 [H2| H2]; [ rewrite H2 | case H2 ]; auto. intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 n1 H3; apply Nat.le_trans with (S n); auto with arith. case in_app_or with (1 := H3); auto. Qed.
imports: Coq(ArithRing)