proposition: Lemma merge_sorted s1 s2 : sorted leT s1 -> sorted leT s2 -> sorted leT (merge s1 s2).
proof: Proof. by rewrite !(eq_sorted leElex); apply/merge_stable_sorted/allrelT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)