proposition: Lemma sorted_ge2_all_ps l: sorted ggen (rcons l 0) -> all (leq 2) l /\ all (leq 1) l.
proof: Proof. rewrite - rev_sorted rev_rcons; move/path_all_llen; rewrite all_rev => h. by split; apply/allP => [x /(allP h) //= /ltnW]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)