proposition: Lemma merge_LocallySorted: forall l1 l2, LocallySorted le l1 -> LocallySorted le l2 -> LocallySorted le (merge (fun x y => bool_decide (x <= y)) l1 l2).
proof: Proof. Proof with auto. intros l1 l2; induction_merge l1 l2; intros ... - rewrite <- (LocallySorted_cons' A le). split. + apply (merge_Forall (le a1) l0 (a2::l3)). * rewrite <- LocallySorted_cons' in H1. now destruct H1. apply le_total. * rewrite <- LocallySorted_cons' in H2. intuition. apply forall_weak with a2 ... apply le_total. intuition. apply le_total. + eapply H0 ... rewrite <- LocallySorted_cons' in H1; intuition. + apply le_total. - rewrite <- LocallySorted_cons'. split. + apply (merge_Forall (le a2) (a1::l0) l3). * rewrite <- LocallySorted_cons' in H1; intuition. apply forall_weak with a1 ... apply le_total. apply le_lt_weak. apply not_le_gt;auto. now constructor. * rewrite <- LocallySorted_cons' in H2; intuition. + eapply H0 ... rewrite <- LocallySorted_cons' in H2; intuition. + apply le_total. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)