proposition: Theorem height_pred_larger_strict : 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 \/ ln = n :: [] /\ l = t :: [].
proof: Proof. intros n n1 ln t l H; generalize n1; elim H; clear H n ln t l n1; auto. intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 n1 H3; left; apply Nat.lt_le_trans with (S n); auto. case in_app_or with (1 := H3). intros H4; apply height_pred_larger with (1 := H); auto. intros H4; apply height_pred_larger with (1 := H1); auto. Qed.
imports: Coq(ArithRing)