proposition: Lemma sorted_glue {A : Type}: forall (A_rel : A -> A -> Prop) (L1 L2 : list A) (a1 a2 : A), Sorted A_rel (L1 ++ (a1 :: nil)) -> Sorted A_rel (a2 :: L2) -> A_rel a1 a2 -> Sorted A_rel ((L1 ++ (a1 :: nil)) ++ (a2 :: L2)).
proof: Proof. induction L1; simpl. constructor; auto. intros. apply Sorted_inv in H. destruct H. constructor. apply IHL1; auto. destruct L1; apply HdRel_inv in H2; constructor; auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset