proposition: Lemma mergeA : associative merge.
proof: Proof. elim=> // x xs IHxs; elim=> // y ys IHys; elim=> [|z zs IHzs] /=. by case: ifP. case: ifP; case: ifP => /= lexy leyz. - by rewrite lexy (leT_tr lexy leyz) -IHxs /= leyz. - by rewrite lexy leyz -IHys. - case: ifP => lexz; first by rewrite -IHxs //= leyz. by rewrite -!/(merge (_ :: _)) IHzs /= lexy. - suff->: leT x z = false by rewrite leyz // -!/(merge (_ :: _)) IHzs /= lexy. by apply/contraFF/leT_tr: leyz; have := leT_total x y; rewrite lexy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)