proposition: Lemma sorted_llen_mkseq_e a n: sorted llen [seq i.*2 | i <- iota a n].
proof: Proof. by apply:sorted_llen_mkseq => u /=; rewrite doubleS !ltnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)