proposition: Lemma sorted_prop f m: sorted ltn (mkseq f m.+1) <-> (forall i, i<m -> f i < f (i.+1)).
proof: Proof. split. move => h i im. move: (map_subseq f (subseq_iota1 im)); rewrite -/(mkseq f m.+1) => pb. have tr_ltn: (transitive ltn) by move => a b c ; apply: ltn_trans. by move: (subseq_sorted tr_ltn pb h)=> /=; rewrite andbT. move => fi. simpl. move: m f fi; elim => [ //= | n hrec f fi /=]. rewrite (fi 0 (ltn0Sn n)) /=. set f' := f \o (addn 1). have fi': (forall i, i < n -> f' i < f' i.+1) by move => i lin; rewrite fi. move: (hrec _ fi'); rewrite map_comp /f' /= addn0 - iotaDl //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)