proposition: Lemma size_sorted a l: sorted gtn (a::l) -> size l <= a ?= iff (l == rev (iota 0 a)).
proof: Proof. elim: l a => [a _|b l Hrec a]. by apply /leqifP; case:a => // a; rewrite iota_Sr rev_rcons //. move => /= /andP [lba /Hrec ha]. split. rewrite (leq_ltn_trans _ lba) //;apply: ha. move: lba; case: a => // a. rewrite ltnS => lab. rewrite iota_Sr rev_rcons add0n eqseq_cons eqSS. have sl: size l <= b by apply: ha. move/leqifP: ha; move: lab; rewrite leq_eqVlt; case /orP => hx. by rewrite -(eqP hx) eqxx; case: eqP => // _ /ltn_eqF ->. rewrite (ltn_eqF hx) /= => _; exact: (ltn_eqF (leq_ltn_trans sl hx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)