proposition: Lemma sorted_of_nth (r : rel A) s (r_trans : transitive r) (r_sorted : sorted r s) : forall x0 a b, a < b < size s -> r (nth x0 s a) (nth x0 s b).
proof: Proof. move=> a0 a b /= /andP [Hab Hbs]. set f := nth a0 s. have Has : a < size s by exact/(leq_ltn_trans _ Hbs)/ltnW. have H : subseq [:: f a ; f b] s. rewrite -(map_nth_iota_id a0 s) (_ : [:: f a; f b] = map f [:: a ; b]) //. apply: map_subseq. rewrite -(subnK Has) addnC iotaD add0n (_ : [:: a; b] = [::a] ++ [::b]) //. apply cat_subseq; rewrite sub1seq mem_iota. - by rewrite add0n leq0n ltnSn. - by rewrite Hab subnKC. by case/andP : (subseq_sorted r_trans H r_sorted). Qed.
imports: mathcomp(all_ssreflect fingroup perm)