proposition: Theorem Sorted_merge : forall l1 l2, Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).
proof: Proof. induction l1; induction l2; intros; simpl; auto. destruct (a <=? a0) eqn:Heq1. - invert H. + simpl. constructor; trivial; rewrite Heq1; constructor. + assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto). clear H0 H3 IHl1; simpl in *. destruct (b <=? a0); constructor; auto || rewrite Heq1; constructor. - assert (a0 <=? a) by (destruct (leb_total a0 a) as [H'|H']; trivial || (rewrite Heq1 in H'; inversion H')). invert H0. + constructor; trivial. + assert (Sorted (merge (a::l1) (b::l))) by auto using IHl1. clear IHl2; simpl in *. destruct (a <=? b); constructor; auto. Qed.
imports: List Setoid Permutation Sorted Orders