proposition: Lemma sorted_llen_mkseq f a n: (forall u, llen (f u) (f u.+1)) -> sorted llen [seq (f i) | i <- iota a n].
proof: Proof. move => h; case: n => // n /=; elim: n a => // n Hrec a /=. rewrite (Hrec a.+1) andbT; exact: (h a). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)