proposition: Lemma merge_permutation: forall l1 l2, Permutation (l1++l2) (merge (fun x y => bool_decide (x <= y)) l1 l2).
proof: Proof. Proof with auto. intros l1 l2; induction_merge l1 l2; intros. - reflexivity. - now rewrite app_nil_r. - simpl. now constructor. - transitivity ((a2::l3)++a1::l0). + apply Permutation_app_comm. + constructor. transitivity (a1::l0++l3) ... apply Permutation_app_comm ... Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)