proposition: Theorem merge_sorted : forall l1 l2:list A, sorted l1 -> sorted l2 -> sorted (merge l1 l2).
proof: Proof. unfold merge in |- *; intros l1 l2 H1 H2; elim (merge_aux_sorted (length l1 + length l2) l1 l2); auto. Qed.
imports: List Lia