proposition: Theorem weight_tree_list_permutation : forall l1 l2 : list (btree A), Permutation l1 l2 -> weight_tree_list l1 = weight_tree_list l2.
proof: Proof. intros l1 l2 H; elim H; auto. simpl in |- *; auto; intros; ring. simpl in |- *; auto; intros; ring. intros l0 l3 l4 H0 H1 H2 H3; apply trans_equal with (1 := H1); auto. Qed.
imports: Coq(ArithRing Sorting.Permutation)