proposition: Lemma map_merge : {morph map f : s1 s2 / merge leT' s1 s2 >-> merge leT s1 s2}.
proof: Proof. elim=> //= x s1 IHs1; elim => [|y s2 IHs2] //=; rewrite f_mono. by case: leT'; rewrite /= ?IHs1 ?IHs2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)