proposition: Theorem build_permutation : forall (l1 l2 : list (btree A)) (t : btree A), build l1 t -> Permutation l1 l2 -> build l2 t.
proof: Proof. intros l1 l2 t H; generalize l2; elim H; clear H l1 l2 t; auto. intros t l2 H; rewrite Permutation_length_1_inv with (1 := H); auto. apply build_one. intros t l1 l2 H H0 H1 l0 H2. apply build_step with (l2 := l2); auto. case H. intros l3 (t1, (t2, (HH1, (HH2, HH3)))). exists l3; exists t1; exists t2; repeat (split; auto). apply Permutation_trans with (2 := HH2); auto. apply Permutation_sym; auto. Qed.
imports: Coq(ArithRing Sorting.Permutation)