proposition: Lemma merge_stable_sorted s1 s2 : allrel leT' s1 s2 -> sorted leT_lex s1 -> sorted leT_lex s2 -> sorted leT_lex (merge s1 s2).
proof: Proof. case: s1 s2 => [|x s1] [|y s2] //=; rewrite allrel_consl allrel_consr /= -andbA. case/and4P => [xy' xs2 ys1 s1s2] xs1 ys2; rewrite -/(merge (_ :: _)). by case: ifP (leT_total x y) => /= xy yx; apply/merge_stable_path; rewrite /= ?(allrel_consl, allrel_consr, xs2, ys1, xy, yx, xy', implybT). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)