proposition: Lemma height_pred_disj_larger2_aux : forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)), height_pred n ln l t -> forall ln1 ln2 a, ln = ln1 ++ a :: ln2 -> (exists n1, In n1 ln1 /\ a <= n1) \/ (exists n1, In n1 ln2 /\ a <= n1) \/ ln = n :: [] /\ l = t :: [].
proof: Proof. intros n ln t l H; elim H; clear H n ln t l. intros n t l ln1 ln2 a; case ln1; simpl in |- *; auto. intros n ln1 ln2 t1 t2 l1 l2 H H0 H1 H2 ln0 ln3 a H3. case app_inv_app with (1 := H3). intros (ln4, H4); auto. cut (ln3 = ln4 ++ ln2); [ intros E1 | apply app_inv_head with (l := ln0 ++ a :: []); repeat rewrite <- app_assoc; simpl in |- *; rewrite <- H3; rewrite H4; rewrite <- app_assoc; auto ]. case H0 with (1 := H4); auto; intros [(n1, (HH1, HH2))| (HH1, HH2)]; auto; clear H0 H2. right; left; exists n1; split; auto; rewrite E1; auto with datatypes. cut (ln0 = [] /\ ln4 = [] /\ a = S n); [ intros (HH3, (HH4, HH5)) | generalize HH1; rewrite H4; case ln0; simpl in |- *; [ case ln4; try (intros; discriminate); (intros HH6; injection HH6; auto) | intros n0 l; case l; simpl in |- *; intros; discriminate ] ]. case height_pred_larger_ex with (1 := H1); auto. intros n1; rewrite <- HH5; intros (HM1, HM2). right; left; exists n1; split; auto; rewrite E1; auto with datatypes. intros (ln4, H4); auto. cut (ln0 = ln1 ++ ln4); [ intros E1 | apply app_inv_tail with (l := a :: ln3); rewrite <- H3; rewrite H4; rewrite <- app_assoc; auto ]. case H2 with (1 := H4); auto; clear H0 H2. intros (n1, (HH1, HH2)); left; exists n1; split; auto; rewrite E1; auto with datatypes. intros [HH1| (HH1, HH2)]; auto. cut (ln3 = [] /\ ln4 = [] /\ a = S n); [ intros (HH3, (HH4, HH5)) | generalize HH1; rewrite H4; case ln4; simpl in |- *; [ case ln3; try (intros; discriminate); (intros HH6; injection HH6; auto) | intros n0 l; case l; simpl in |- *; intros; discriminate ] ]. case height_pred_larger_ex with (1 := H); auto. intros n1; rewrite <- HH5; intros (HM1, HM2). left; exists n1; split; auto; rewrite E1; auto with datatypes. Qed.
imports: Coq(ArithRing)