proposition: Lemma Sorted_list_merge `{!Total R} l1 l2 : Sorted R l1 → Sorted R l2 → Sorted R (list_merge R l1 l2).
proof: Proof. intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1]; induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl; repeat case_decide; repeat match goal with H : ¬R _ _ |- _ => apply total_not in H end; constructor; eauto using HdRel_list_merge, HdRel_cons. Qed.
imports: stdpp(options)