proposition: Lemma srt_m2s n (m : 'X_{1..n}): isorted (m2s m).
proof: Proof. have h (T : eqType) (leT : rel T) (s : seq T) (F : T -> nat) x: reflexive leT -> transitive leT -> path leT x s -> path leT x (flatten [seq nseq (F x) x | x <- s]). * move=> leTxx leT_tr; elim: s x => //= y s ih x /andP[le_xy pt_ys]. case: (F y)=> /= [|k]; first apply/ih. rewrite path_min_sorted; do ?apply: (introT allP). exact/(path_sorted (x := y)). move=> z z_in_s /=; apply/(leT_tr y)=> //. by move/order_path_min: pt_ys => /(_ leT_tr) /allP /(_ _ z_in_s). rewrite le_xy /= cat_path; apply/andP; split. by elim: k=> //= k ->; rewrite leTxx. by have ->: last y (nseq k y) = y; [elim: k | apply/ih]. case: n m=> [|n] m. case: m => t /=; rewrite /m2s; have ->//: enum 'I_0 = [::]. by apply/size0nil; rewrite size_enum_ord. apply/(path_sorted (x := val (0 : 'I_n.+1))). pose P := [rel i j : 'I_n.+1 | i <= j]. rewrite (map_path (e' := P) (b := xpred0)) //=; last first. by apply/hasP; case. apply/h; try solve [exact/leqnn | exact/leq_trans]. rewrite -(map_path (h := val) (e := leq) (b := xpred0)) //. rewrite val_enum_ord /= path_min_sorted ?iota_sorted//; do ?exact: (introT allP). by apply/hasP; case. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg