proposition: Theorem ordered_sum_leaves_eq : forall (A : Type) (f : A -> nat) (l1 l2 : list (btree A)), Permutation l1 l2 -> ordered (sum_order f) l1 -> ordered (sum_order f) l2 -> map (sum_leaves f) l1 = map (sum_leaves f) l2.
proof: Proof. intros A f l1 l2 H H0 H1. apply ordered_perm_antisym_eq with (order := le). exact Nat.le_trans. exact Nat.le_antisymm. apply Permutation_map; auto. apply ordered_map_inv; auto. apply ordered_map_inv; auto. Qed.
imports: Coq(ArithRing Sorting.Permutation)