proposition: Lemma spec_sorted_rcons l i: (spec_sorted (rcons l i)) = (sorted lespec (i:: rev l)) && (i <= 1).
proof: Proof. by rewrite - {1} (revK ((rcons l i))) spec_sorted_rev rev_rcons /= !eqSS leqn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)