proposition: Lemma sorted_cat (l k : seq A) (r : @rel A) : sorted r l -> sorted r k -> (forall a, a \in l -> forall b, b \in k -> r a b) -> sorted r (l ++ k).
proof: Proof. move=> Hl Hk H. destruct l => //. rewrite /sorted /= cat_path. rewrite /sorted in Hl. apply/andP; split => //. destruct k => //. rewrite /sorted in Hk. rewrite /= Hk andbC /=. apply H. by rewrite mem_last. by rewrite in_cons eqxx. Qed.
imports: mathcomp(all_ssreflect fingroup perm)