proposition: Lemma sorted_llen_succ l: sorted llen (succ_seq l) = sorted llen l.
proof: Proof. by case: l => //= a l; elim: l a => // a l H b /=; rewrite ltnS H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)