proposition: Theorem height_pred_shrink : forall (n a b : nat) (ln1 ln2 : list nat) (t t1 t2 : btree A) (l1 l2 : list (btree A)), height_pred n (ln1 ++ a :: b :: ln2) (l1 ++ t1 :: t2 :: l2) t -> (forall n1 : nat, In n1 ln1 -> n1 < a) -> (forall n1 : nat, In n1 (b :: ln2) -> n1 <= a) -> length ln1 = length l1 -> height_pred n (ln1 ++ pred a :: ln2) (l1 ++ node t1 t2 :: l2) t.
proof: Proof. intros n a b ln1 ln2 t t1 t2 l1 l2 H H0 H1 H2; apply height_pred_shrink_aux with (1 := H) (b := b); auto. Qed.
imports: Coq(ArithRing)