proposition: Theorem height_pred_weight : forall (n : nat) (ln : list nat) (t : btree A) (l : list (btree A)), height_pred n ln l t -> n * sum_leaves f t + weight_tree f t = prod2list f ln l.
proof: Proof. intros n ln t l H; elim H; simpl in |- *; auto. intros n0 ln1 ln2 t1 t2 l1 l2 H0 H1 H2 H3. rewrite prod2list_app; auto with arith. rewrite <- H3; rewrite <- H1; ring. apply height_pred_length with (1 := H0); auto. Qed.
imports: Coq(ArithRing)