proposition: Lemma DUR_positive i: 0 < v i.
proof: Proof. case: (posnP (v i)) => // h. have ha j: spec_sorted (rev(iota 0 j)). rewrite spec_sorted_rev; apply/andP; split; last by case:j. by elim: j 0 => // j H k /=; move:(H k.+1); case j => // m /=; rewrite eqxx. move:(v_unique (ha i)(ha i.+1)). rewrite /Zval_v !sum_rev iota_Sr sum_rcons h add0n => H. have: i \in (iota 0 i) by rewrite (rev_inj (H (erefl _))) mem_rcons inE eqxx. by rewrite mem_iota // ltnn andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)