proposition: Theorem height_pred_disj_larger : forall (n a : nat) (ln1 ln2 : list nat) (t : btree A) (l : list (btree A)), height_pred n (ln1 ++ a :: ln2) l t -> (forall n1 : nat, In n1 ln1 -> n1 < a) -> (forall n1 : nat, In n1 ln2 -> n1 <= a) -> (exists ln3, ln2 = a :: ln3) \/ (ln1 = [] /\ a = n /\ ln2 = []) /\ l = t :: [].
proof: Proof. intros n a ln1 ln2 t l H H0 H1; case height_pred_disj_larger_aux with (a := a) (ln1 := ln1) (ln2 := ln2) (1 := H); auto; case ln1; simpl in |- *; [ intros (HH1, HH2); injection HH1; auto | intros n0 l1; case l1; simpl in |- *; intuition; try discriminate ]. Qed.
imports: Coq(ArithRing)