proposition: Theorem weight_tree_list_node : forall (t1 t2 : btree A) (l : list (btree A)), weight_tree_list (node t1 t2 :: l) = sum_leaves t1 + sum_leaves t2 + weight_tree_list (t1 :: t2 :: l).
proof: Proof. intros t1 t2 l; simpl in |- *; ring. Qed.
imports: Coq(ArithRing Sorting.Permutation)