proposition: Theorem height_pred_disj_larger2 : forall (n a : nat) (ln1 ln2 : list nat) (t : btree A) (l : list (btree A)), height_pred n (ln1 ++ a :: ln2) l t -> (exists n1, In n1 ln1 /\ a <= n1) \/ (exists n1, In n1 ln2 /\ a <= n1) \/ (ln1 = [] /\ a = n /\ ln2 = []) /\ l = t :: [].
proof: Proof. intros n a ln1 ln2 t l H; case height_pred_disj_larger2_aux with (a := a) (ln1 := ln1) (ln2 := ln2) (1 := H); auto. intros [H1| (H1, H2)]; auto. generalize H1 H2; case ln1; simpl in |- *; [ intros H3; injection H3; auto with datatypes | idtac ]. intros H0 H4 H5; repeat right; auto. intros n0 l0; case l0; simpl in |- *; intros; discriminate. Qed.
imports: Coq(ArithRing)