proposition: Lemma seq_prednK l: all (leq 1) l -> l = succ_seq (pred_seq l).
proof: Proof. by elim:l => // a l H /= /andP [] /prednK -> /H <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)